Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
import Mathlib.Tactic.TypeStar
import Mathlib.Tactic.SuccessIfFailWithMsg
private axiom test_sorry : ∀ {α}, α
noncomputable example (_x _y : Type*) : test_sorry := by
success_if_fail_with_msg
"type mismatch
_y
has type
Type u_2 : Type (u_2 + 1)
but is expected to have type
Type u_1 : Type (u_1 + 1)" (exact _x = _y)
exact test_sorry
noncomputable example (_x : Sort*) : test_sorry := by
Prop
Type : Type 1
Sort u_1 : Type u_1" (exact _x = Prop)
noncomputable example : test_sorry := by
y
Type u_1 : Type (u_1 + 1)" (exact ∀ x y : Type*, x = y)
Sort u_1 : Type u_1" (exact ∀ x : Sort*, x = Prop)
