From eb86a19031f4f8afd2ab1a0c318236a9cb836320 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 8 Jul 2024 13:27:30 +0200
Subject: [PATCH] test: no more axioms are necessary

---
 Test/Bv/AxiomCheck.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

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