diff --git a/Test/Bv/AxiomCheck.lean b/Test/Bv/AxiomCheck.lean index 5cdb7ee9..cf890b0f 100644 --- a/Test/Bv/AxiomCheck.lean +++ b/Test/Bv/AxiomCheck.lean @@ -7,11 +7,7 @@ theorem bv_axiomCheck (x y : BitVec 1) : x + y = y + x := by bv_decide /-- -info: 'bv_axiomCheck' depends on axioms: [propext, - Classical.choice, - Lean.ofReduceBool, - Quot.sound, - AIG.RelabelNat.State.Inv2.property] +info: 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/ #guard_msgs in #print axioms bv_axiomCheck