@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...
@kamatsu8 Interesting idea... not sure I’d use Ivor any more though - the API is horrible!
-
-
@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... -
@edwinbrady includes holes and unification so that interactive proof construction is possible. - 2 more replies
New conversation -
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.