40 lines
959 B
Text
40 lines
959 B
Text
shadow.lean:6: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:10: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:13:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u_1
|
||
inst✝² : Inhabited α
|
||
inst✝¹ inst : α
|
||
β✝¹ δ✝¹ : Type
|
||
⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
|
||
shadow.lean:17:0: error: don't know how to synthesize placeholder
|
||
context:
|
||
α : Type u_1
|
||
inst.16 : Inhabited α
|
||
inst inst : α
|
||
β.41 δ.42 : Type
|
||
⊢ α → β.41 → δ.42 → α×β.41×δ.42
|
||
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
|
||
⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
|