News for hackers. Stuff that matters.

A comment on Theorem Proving in Lean.

Re:Theorem Proving in Lean by tmpmov on Monday May 28, 2018 @11:12PM (#17176198)
Was there a reason for the move away from HoTT? I seem to recall looking this up a while ago but didn't find a solid answer. Was there a fork version 2 that continues development with HoTT?
[ Parent | on HN ]
Re:Theorem Proving in Lean by im_down_w_otp on Monday May 28, 2018 @11:20PM (#17176225)
This was a discussion I remember coming across not long ago when I had the same question: https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIz...

There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3

Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think Lean 2 started life intending to handle HoTT either.

[ Parent | on HN ]