test output

Author: kim-em

MathlibTest/fast_instance.lean

@@ -117,7 +117,7 @@ abbrev dec1 : Decidable It := isTrue sorry
 #guard_msgs in
 def dec2 : Decidable It := isTrue sorry
 
-/-- info: @Dec.mk It (@isTrue It ⋯) : Dec It -/
+/-- info: @Dec.mk It (@isTrue It _check._proof_1) : Dec It -/
 #guard_msgs (info, drop warning) in
 set_option pp.explicit true in
 #check fast_instance% { dec := dec1 : Dec It }