We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 04e1661 commit a265977Copy full SHA for a265977
src/Lean/Elab/Tactic/BVAckermannize.lean
@@ -7,6 +7,8 @@ This file implements lazy ackermannization [1, 2]
7
8
[1] https://lara.epfl.ch/w/_media/model-based.pdf
9
[2] https://leodemoura.github.io/files/oregon08.pdf
10
+[3] https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr.cpp#L206
11
+[4]https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr_model_constructor.cpp#L344
12
-/
13
prelude
14
import Std.Tactic.BVDecide.Bitblast
0 commit comments