Update name of getLsb_cons to getLsbD_cons

ufmg-smite · Nov 14, 2024 · 877ee4a · 877ee4a
1 parent 8bc677e
commit 877ee4a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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