f47f605039
It had two problems: - It was preventing coercions from being applied. - It was compromising error recovery. The body of the lambda was not being elaborated when the exception was thrown. The new error message is more verbose and potentially confusing, but it is better than the one produced this morning.
34 lines
1.2 KiB
Text
34 lines
1.2 KiB
Text
mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
|
|
fun (a : ?m) (b : ?m a) => ?m a b
|
|
has type
|
|
(a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
|
|
but is expected to have type
|
|
a✝ * b✝ = b✝ * a✝ : Prop
|
|
the following variables have been introduced by the implicit lamda feature
|
|
a✝ : Bool
|
|
b✝ : Bool
|
|
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
|
|
mulcommErrorMessage.lean:11:22-11:25: error: type mismatch
|
|
rfl
|
|
has type
|
|
true = true : Prop
|
|
but is expected to have type
|
|
true = false : Prop
|
|
mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
|
|
fun (a b : Bool) => Bool.casesOn a (?m a b) (?m a b)
|
|
has type
|
|
(a b : Bool) → ?m a b a : Sort (imax 1 1 ?u)
|
|
but is expected to have type
|
|
a✝ * b✝ = b✝ * a✝ : Prop
|
|
the following variables have been introduced by the implicit lamda feature
|
|
a✝ : Bool
|
|
b✝ : Bool
|
|
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
|
|
mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch
|
|
Bool.casesOn a ?m (Bool.casesOn b ?m ?m)
|
|
argument
|
|
Bool.casesOn b ?m ?m
|
|
has type
|
|
?m a b b : Sort ?u
|
|
but is expected to have type
|
|
?m a b true : Sort ?u
|