From 877ee4afaf2a3f771918f4a35e5cb5ebe0b2c314 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 14 Nov 2024 15:22:40 +0100 Subject: [PATCH] Update name of getLsb_cons to getLsbD_cons --- Smt/Reconstruct/BitVec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean index e8b6126b..6670a140 100644 --- a/Smt/Reconstruct/BitVec.lean +++ b/Smt/Reconstruct/BitVec.lean @@ -274,7 +274,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let h : Q(decide (BitVec.beq $x $y) = decide $p) ← Meta.mkFreshExprMVar q(decide (BitVec.beq $x $y) = @decide $p $hp) let mv ← Bool.boolify h.mvarId! let ds := [``BitVec.beq, ``BitVec.beq.go] - let ts := [``BitVec.getLsb_cons, ``Nat.succ.injEq] + let ts := [``BitVec.getLsbD_cons, ``Nat.succ.injEq] let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEqDiff, ``reduceIte] let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {} let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems @@ -290,7 +290,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let h : Q((BitVec.adc' $x $y false).snd = $z) ← Meta.mkFreshExprMVar q((BitVec.adc' $x $y false).snd = $z) let mv ← Bool.boolify h.mvarId! let ds := [``BitVec.adc', ``BitVec.adcb', ``BitVec.iunfoldr, ``Fin.hIterate, ``Fin.hIterateFrom] - let ts := [``BitVec.getLsb_cons, ``Nat.succ.injEq] + let ts := [``BitVec.getLsbD_cons, ``Nat.succ.injEq] let ps := [``Nat.reduceAdd, ``Nat.reduceLT, ``reduceDIte, ``reduceIte] let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {} let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems