You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
addOne : Nat -> Nat
addOne n1 =
use Nat +
n1 + 1
-- parses the same as:
addOne' : Nat -> Nat
addOne' n1 =
use Nat + n1 +
1
-- when it was meant to parse as:
addOne'' : Nat -> Nat
addOne'' n =
use Nat +
n + 1
> addOne 5
> addOne' 5
> addOne'' 5
Loading changes detected in scratch.u.
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
addOne : Nat -> Nat
addOne' : Nat -> Nat
addOne'' : Nat -> Nat
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
17 | > addOne 5
⧩
1
18 | > addOne' 5
⧩
1
19 | > addOne'' 5
⧩
6
UCM should at least give an error, not split the use line arbitrarily at the nat literal.
Screenshots
If applicable, add screenshots to help explain your problem.
Environment (please complete the following information):
0.5.29
Additional context
The text was updated successfully, but these errors were encountered:
Describe and demonstrate the bug
UCM should at least give an error, not split the use line arbitrarily at the nat literal.
Screenshots
If applicable, add screenshots to help explain your problem.
Environment (please complete the following information):
Additional context
The text was updated successfully, but these errors were encountered: