test: no more axioms are necessary

leanprover · Jul 8, 2024 · eb86a19 · eb86a19
1 parent bcb0a3a
commit eb86a19
Showing 1 changed file with 1 addition and 5 deletions.
diff --git 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