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>
62 lines
1.4 KiB
Text
62 lines
1.4 KiB
Text
doErrorMsg.lean:4:2-4:13: error: Type mismatch
|
|
IO.getStdin
|
|
has type
|
|
BaseIO IO.FS.Stream
|
|
but is expected to have type
|
|
IO Unit
|
|
doErrorMsg.lean:16:19-16:21: error: Type mismatch
|
|
f1
|
|
has type
|
|
ExceptT String (StateT Nat Id) Nat
|
|
but is expected to have type
|
|
ExceptT String (StateT Nat Id) String
|
|
doErrorMsg.lean:20:19-20:24: error: Type mismatch
|
|
f2 10
|
|
has type
|
|
ExceptT String (StateT Nat Id) Nat
|
|
but is expected to have type
|
|
ExceptT String (StateT Nat Id) String
|
|
doErrorMsg.lean:24:10-24:12: error: Type mismatch
|
|
f2
|
|
has type
|
|
Nat → ExceptT String (StateT Nat Id) Nat
|
|
but is expected to have type
|
|
ExceptT String (StateT Nat Id) ?m
|
|
doErrorMsg.lean:25:2-25:4: error: Type mismatch
|
|
f1
|
|
has type
|
|
ExceptT String (StateT Nat Id) Nat
|
|
but is expected to have type
|
|
ExceptT String (StateT Nat Id) String
|
|
doErrorMsg.lean:29:7-29:12: error: Type mismatch
|
|
false
|
|
has type
|
|
Bool
|
|
but is expected to have type
|
|
Nat
|
|
doErrorMsg.lean:30:2-30:3: error: Type mismatch
|
|
n
|
|
has type
|
|
Nat
|
|
but is expected to have type
|
|
Char
|
|
doErrorMsg.lean:30:14-30:19: error: Type mismatch
|
|
false
|
|
has type
|
|
Bool
|
|
but is expected to have type
|
|
Nat
|
|
doErrorMsg.lean:31:13-31:18: error: Application type mismatch: The argument
|
|
false
|
|
has type
|
|
Bool
|
|
but is expected to have type
|
|
Nat
|
|
in the application
|
|
Prod.mk false
|
|
doErrorMsg.lean:32:3-32:13: error: Type mismatch
|
|
n
|
|
has type
|
|
Nat
|
|
but is expected to have type
|
|
Char
|