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>
67 lines
2.9 KiB
Plaintext
67 lines
2.9 KiB
Plaintext
doNotation1.lean:5:0-5:1: error: Variable `y` cannot be mutated. Only variables declared using `let mut` can be mutated.
|
||
If you did not intend to mutate but define `y`, consider using `let y` instead
|
||
doNotation1.lean:9:3-9:4: error: Variable `y` cannot be mutated. Only variables declared using `let mut` can be mutated.
|
||
If you did not intend to mutate but define `y`, consider using `let y` instead
|
||
doNotation1.lean:13:2-13:3: error: Variable `p` cannot be mutated. Only variables declared using `let mut` can be mutated.
|
||
If you did not intend to mutate but define `p`, consider using `let p` instead
|
||
doNotation1.lean:21:7-21:23: error: Type mismatch
|
||
Vector'.cons 1 v
|
||
has type
|
||
Vector' Nat (n + 1)
|
||
but is expected to have type
|
||
Vector' Nat n
|
||
doNotation1.lean:26:7-26:11: error: Type mismatch
|
||
true
|
||
has type
|
||
Bool
|
||
but is expected to have type
|
||
Nat
|
||
doNotation1.lean:36:2-36:7: error: `break` must be nested inside a loop
|
||
doNotation1.lean:40:2-40:10: error: `continue` must be nested inside a loop
|
||
doNotation1.lean:44:0-44:9: warning: This `do` element and its control-flow region are dead code. Consider removing it.
|
||
def f10 : Nat → IO Unit :=
|
||
fun x => IO.println x
|
||
doNotation1.lean:54:0-54:13: error: Type mismatch
|
||
IO.mkRef true
|
||
has type
|
||
BaseIO (IO.Ref Bool)
|
||
but is expected to have type
|
||
IO Unit
|
||
doNotation1.lean:58:7-58:11: error: Application type mismatch: The argument
|
||
true
|
||
has type
|
||
Bool
|
||
but is expected to have type
|
||
Unit
|
||
in the application
|
||
pure true
|
||
doNotation1.lean:66:2-66:20: error: Type mismatch
|
||
IO.println "hello"
|
||
has type
|
||
IO Unit
|
||
but is expected to have type
|
||
IO Bool
|
||
doNotation1.lean:73:0-73:18: warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
|
||
doNotation1.lean:78:0-78:32: warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
|
||
doNotation1.lean:78:21-78:31: error: typeclass instance problem is stuck
|
||
ToString ?m
|
||
|
||
Note: Lean will not try to resolve this typeclass instance problem because the type argument to `ToString` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
|
||
|
||
Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
|
||
doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type PUnit, but the rest of the `do` sequence expected List (Nat × Nat).
|
||
doNotation1.lean:83:7-83:9: error: Application type mismatch: The argument
|
||
()
|
||
has type
|
||
Unit
|
||
but is expected to have type
|
||
List (Nat × Nat)
|
||
in the application
|
||
pure ()
|
||
doNotation1.lean:82:0-83:9: error: Type mismatch
|
||
PUnit.unit
|
||
has type
|
||
PUnit
|
||
but is expected to have type
|
||
List (Nat × Nat)
|