12 lines
429 B
Text
12 lines
429 B
Text
def1.lean:5:16: error: "eliminator" elaborator type mismatch, term
|
|
rfl
|
|
has type
|
|
?m_2 = ?m_2
|
|
but is expected to have type
|
|
f b = f c
|
|
Additional information:
|
|
def1.lean:5:16: context: the inferred motive for the eliminator-like application is
|
|
λ (_x : A), f _x = f c
|
|
def1.lean:5:3: context: the inferred motive for the eliminator-like application is
|
|
λ (_x : A), f a = f c
|
|
def1.lean:4:0: error: unknown declaration 'sorry'
|