mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
15 lines
279 B
Plaintext
15 lines
279 B
Plaintext
elseifDoErrorPos.lean:5:10-5:11: error: Application type mismatch: The argument
|
|
x
|
|
has type
|
|
Nat
|
|
but is expected to have type
|
|
Prop
|
|
in the application
|
|
@ite ?m x
|
|
elseifDoErrorPos.lean:8:11-8:14: error: Type mismatch
|
|
"a"
|
|
has type
|
|
String
|
|
but is expected to have type
|
|
Nat
|