News for hackers. Stuff that matters.

A comment on The Z3 Theorem Prover released under MIT license. Parent comment

Re:The Z3 Theorem Prover released under MIT license by NotableAlamode on Thursday March 26, 2015 @07:11PM (#9273778)
Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?
[ Parent | on HN ]

There are no comments on this comment yet.