Show HN: Algebruh - Cross-check arithmetic claims with Z3, cvc5, and Lean github.com 14 points by modinfo 3 days ago
okigan 2 days ago Readme is mostly install and usage information but not much above the use case.OP - could you fill in why/when one would use it?
derdi 2 days ago Nice, but what is the motivation for this? That the syntax is perceived to be nicer than SMT-LIB format? Or that Lean can get involved? Differential testing? Just for fun?
Readme is mostly install and usage information but not much above the use case.
OP - could you fill in why/when one would use it?
Nice, but what is the motivation for this? That the syntax is perceived to be nicer than SMT-LIB format? Or that Lean can get involved? Differential testing? Just for fun?