Conversation

дэн
@dan_abramov
don’t know what this is but it sure looks beautiful
Quote Tweet
Liam O'Connor
@kamatsu8
·
The next version of Holbert will include: Support for elimination rules, support for rewriting with equalities, a revamped goal interface, prose style proofs and now including dark mode!
Show this thread
Image
5
32
Brendan Zabarauskas
@brendanzab
Replying to
@dan_abramov
Alfa is another tool worth checking out! Lets you swap between different projections of a proof, including natural deduction: cth.altocumulus.org/~hallgren/Alfa
@kamatsu8
has brought this up in conversation with me in the past too:
Quote Tweet
Brendan Zabarauskas
@brendanzab
·
Replying to @kamatsu8
Yeah Alfa is suuuper neat! I'm a big fan! cse.chalmers.se/~hallgren/Alfa/
Image
Twitter Web App
Liam O'Connor
@kamatsu8
Replying to
@brendanzab
and
@dan_abramov
Alfa is great but it's still a type theory tool first and presentation tool second. Most PL/CS books that use a proof assistant spend >50% of the book talking about the mechanics of the tool. Holbert aims to bring that down as low as possible. With Alfa it would still be >50%.
1
1
Show replies