49 lines
1.3 KiB
Text
49 lines
1.3 KiB
Text
shadow.lean:4:0: error: type mismatch
|
||
h
|
||
has type
|
||
x✝¹=x✝¹
|
||
but it is expected to have type
|
||
x=x
|
||
failed to synthesize instance
|
||
CoeT (x✝¹=x✝¹) _ (x=x)
|
||
shadow.lean:8:0: error: type mismatch
|
||
h
|
||
has type
|
||
x=x
|
||
but it is expected to have type
|
||
x=x
|
||
failed to synthesize instance
|
||
CoeT (x=x) _ (x=x)
|
||
with resulting expansion
|
||
section set_option pp.sanitizeNames false theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
|
||
h -- this error is confusing because we have disabled `pp.sanitizeNames`
|
||
|
||
end
|
||
while expanding
|
||
set_option pp.sanitizeNames false in
|
||
theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
|
||
h
|
||
shadow.lean:12:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u_1
|
||
inst✝² : Inhabited α
|
||
inst✝¹ inst : α
|
||
β✝¹ δ✝¹ : Type
|
||
⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
|
||
shadow.lean:16:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u_1
|
||
inst.19 : Inhabited α
|
||
inst inst : α
|
||
β.44 δ.45 : Type
|
||
⊢ α → β.44 → δ.45 → α×β.44×δ.45
|
||
shadow.lean:20:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u_1
|
||
β : Sort u_2
|
||
inst✝² : α
|
||
b : β
|
||
inst : α
|
||
inst✝¹ : Inhabited α
|
||
β✝¹ δ✝¹ : Type
|
||
⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
|