fix tests

alexkeizer · Oct 9, 2024 · 0bcacaa · 0bcacaa
1 parent 6ef5a8c
commit 0bcacaa
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Test/DeadWrap.lean b/Test/DeadWrap.lean
@@ -8,11 +8,11 @@ namespace Test
 data DeadWrap (α : Type) β
   | mk : α → DeadWrap α β
 
-/-- info: 'Test.DeadWrap.Base' does not depend on any axioms  -/
+/-- info: 'Test.DeadWrap.Base' depends on axioms: [propext, Quot.sound] -/
 #guard_msgs in
   #print axioms DeadWrap.Base
 
-/-- info: Test.DeadWrap.mk {α β : Type} (a✝ : α) : DeadWrap α β -/
+/-- info: Test.DeadWrap.mk {α β : Type} : α → DeadWrap α β -/
 #guard_msgs in
   #check DeadWrap.mk
 

diff --git a/Test/Wrap.lean b/Test/Wrap.lean
@@ -7,7 +7,7 @@ namespace Test
 data Wrap α
   | mk : α → Wrap α
 
-/-- info: Test.Wrap.mk {α : Type} (a✝ : α) : Wrap α -/
+/-- info: Test.Wrap.mk {α : Type} : α → Wrap α -/
 #guard_msgs in
   #check Wrap.mk