|
@bentnib | |||||
|
Proof editor now shows you the proof tree you're building as you type proof commands personal.cis.strath.ac.uk/robert.atkey/c… pic.twitter.com/WCwj8ohPSN
|
||||||
|
||||||
|
Greg Michaelson
@GregMichaelson1
|
7. stu |
|
That's a very cool piece of work. I could have done with that a long time ago in lots of different contexts.
|
||
|
||
|
|
Bob Atkey
@bentnib
|
7. stu |
|
Thanks! You might enjoy the coursework I'm getting the students to do with it: personal.cis.strath.ac.uk/robert.atkey/c…
|
||
|
|
||
|
Geoffrey Litt
@geoffreylitt
|
7. stu |
|
I'm taking a lecture course that involves proof trees on powerpoint slides + chalkboards, wish it used this instead!
|
||
|
|
||
|
Neil Ghani
@Anarchia45
|
7. stu |
|
Gorgeous!
|
||
|
|
||
|
Jan is on Action Short of #UCUStrikes.
@jfdm
|
7. stu |
|
i should show this to my project student...
|
||
|
|
||
|
|
Bob Atkey
@bentnib
|
8. stu |
|
The proof language is a disguised version of the simply-typed lambda calculus, in beta-normal form. The editor itself is written in OCaml and compiled to JS using js_of_ocaml.
|
||
|
|
||