Comment by nextaccountic
7 hours ago
The authors of Lean also wrote a smt solver (Z3). Other proof languages like F* use Z3 to prove its things
Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind
7 hours ago
The authors of Lean also wrote a smt solver (Z3). Other proof languages like F* use Z3 to prove its things
Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind
No comments yet
Contribute on Hacker News ↗