15 lines
227 B
Text
15 lines
227 B
Text
string ↣ name : mk_simple_name
|
|
A ↣ B : f
|
|
g a : B
|
|
sec2.lean:13:6: error: type mismatch at application
|
|
g a
|
|
term
|
|
a
|
|
has type
|
|
A
|
|
but is expected to have type
|
|
B
|
|
string ↣ name : mk_simple_name
|
|
A ↣ B : f
|
|
g a : B
|
|
g a : B
|