From a2659770ed3ead80f5ddb499295caa72c7960ea6 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Sat, 28 Sep 2024 17:05:26 -0500 Subject: [PATCH] chore: add more sources --- src/Lean/Elab/Tactic/BVAckermannize.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Elab/Tactic/BVAckermannize.lean b/src/Lean/Elab/Tactic/BVAckermannize.lean index 4ed3456c4c3a..e6e3b957a106 100644 --- a/src/Lean/Elab/Tactic/BVAckermannize.lean +++ b/src/Lean/Elab/Tactic/BVAckermannize.lean @@ -7,6 +7,8 @@ This file implements lazy ackermannization [1, 2] [1] https://lara.epfl.ch/w/_media/model-based.pdf [2] https://leodemoura.github.io/files/oregon08.pdf +[3] https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr.cpp#L206 +[4]https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr_model_constructor.cpp#L344 -/ prelude import Std.Tactic.BVDecide.Bitblast