Update Prop.lean (#133)

Fix a minor bug.
ufmg-smite · Oct 6, 2024 · 0ad8dee · 0ad8dee
1 parent 563b1be
commit 0ad8dee
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean
@@ -81,7 +81,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     addThm q(($p → $q) = (¬$p ∨ $q)) q(@Prop.bool_impl_elim $p $q)
   | .BOOL_OR_TRUE =>
-    let args ← reconstructArgs pf.getArguments
+    let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_true) args)
   | .BOOL_OR_FALSE =>
     let args ← reconstructArgs pf.getArguments[1:]