unison/unison-src/transcripts/update-term-with-dependent-to-different-type.output.md

84 lines
1.3 KiB
Markdown
Raw Permalink Normal View History

``` ucm
scratch/main> builtins.merge
Done.
```
``` unison
foo : Nat
foo = 5
bar : Nat
bar = foo + 10
```
``` ucm
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`:
bar : Nat
foo : Nat
```
``` ucm
scratch/main> add
⍟ I've added these definitions:
bar : Nat
foo : Nat
```
``` unison
foo : Int
foo = +5
```
``` ucm
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 names already exist. You can `update` them to your
new definition:
foo : Int
```
``` ucm
scratch/main> update
2023-11-14 06:36:03 +03:00
Okay, I'm searching the branch for code that needs to be
updated...
That's done. Now I'm making sure everything typechecks...
Typechecking failed. I've updated your scratch file with the
definitions that need fixing. Once the file is compiling, try
`update` again.
```
``` unison:added-by-ucm scratch.u
2024-07-23 20:45:16 +03:00
foo : Int
foo = +5
2024-08-02 00:49:45 +03:00
-- The definitions below no longer typecheck with the changes above.
-- Please fix the errors and try `update` again.
2024-07-23 20:45:16 +03:00
2024-01-05 02:04:28 +03:00
bar : Nat
bar =
use Nat +
foo + 10
```