@edwinbrady BTW I was thinking of making use of your old Ivor code to implement a beginner's graphical theorem prover for my PLs class...
-
-
Replying to @edwinbrady
@edwinbrady It's not so bad -- I'm used to HOL style theorem provers. I was just looking for a simple type theory implementation that...1 reply 0 retweets 0 likes -
Replying to @kamatsu8
@edwinbrady includes holes and unification so that interactive proof construction is possible.1 reply 0 retweets 0 likes -
Replying to @kamatsu8
@edwinbrady Implementing it myself seemed like a waste, but Idris and Agda both have very sophisticated implementations.2 replies 0 retweets 0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.