News for hackers. Stuff that matters.

A comment on Theorem Proving in Lean [pdf]. Parent comment

Re:Theorem Proving in Lean [pdf] by xvilka on Sunday September 29, 2019 @10:16PM (#21111201)
It's notable, that Coq has more libraries and useful extensions. And they merged Ltac2 into the master, so tactics writing should be better soon.
[ Parent | on HN ]

There are no comments on this comment yet.