mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
Merge pull request #5042 from sellout/numbered-args-delete.namespace
This commit is contained in:
commit
2540774b2f
40
unison-src/transcripts/fix1532.md
Normal file
40
unison-src/transcripts/fix1532.md
Normal file
@ -0,0 +1,40 @@
|
||||
```ucm
|
||||
.> builtins.merge
|
||||
```
|
||||
|
||||
First, lets create two namespaces. `foo` and `bar`, and add some definitions.
|
||||
|
||||
```unison
|
||||
foo.x = 42
|
||||
foo.y = 100
|
||||
bar.z = x + y
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> add
|
||||
```
|
||||
|
||||
Let's see what we have created...
|
||||
|
||||
```ucm
|
||||
.> ls
|
||||
```
|
||||
|
||||
Now, if we try deleting the namespace `foo`, we get an error, as expected.
|
||||
|
||||
```ucm:error
|
||||
.> delete.namespace foo
|
||||
```
|
||||
|
||||
Any numbered arguments should refer to `bar.z`.
|
||||
|
||||
```ucm
|
||||
.> debug.numberedArgs
|
||||
```
|
||||
|
||||
We can then delete the dependent term, and then delete `foo`.
|
||||
|
||||
```ucm
|
||||
.> delete.term 1
|
||||
.> delete.namespace foo
|
||||
```
|
89
unison-src/transcripts/fix1532.output.md
Normal file
89
unison-src/transcripts/fix1532.output.md
Normal file
@ -0,0 +1,89 @@
|
||||
```ucm
|
||||
.> builtins.merge
|
||||
|
||||
Done.
|
||||
|
||||
```
|
||||
First, lets create two namespaces. `foo` and `bar`, and add some definitions.
|
||||
|
||||
```unison
|
||||
foo.x = 42
|
||||
foo.y = 100
|
||||
bar.z = x + y
|
||||
```
|
||||
|
||||
```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.z : Nat
|
||||
foo.x : Nat
|
||||
foo.y : Nat
|
||||
|
||||
```
|
||||
```ucm
|
||||
.> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
bar.z : Nat
|
||||
foo.x : Nat
|
||||
foo.y : Nat
|
||||
|
||||
```
|
||||
Let's see what we have created...
|
||||
|
||||
```ucm
|
||||
.> ls
|
||||
|
||||
1. bar/ (1 term)
|
||||
2. builtin/ (469 terms, 74 types)
|
||||
3. foo/ (2 terms)
|
||||
|
||||
```
|
||||
Now, if we try deleting the namespace `foo`, we get an error, as expected.
|
||||
|
||||
```ucm
|
||||
.> delete.namespace foo
|
||||
|
||||
⚠️
|
||||
|
||||
I didn't delete the namespace because the following
|
||||
definitions are still in use.
|
||||
|
||||
Dependency Referenced In
|
||||
x 1. bar.z
|
||||
|
||||
y 2. bar.z
|
||||
|
||||
If you want to proceed anyways and leave those definitions
|
||||
without names, use delete.namespace.force
|
||||
|
||||
```
|
||||
Any numbered arguments should refer to `bar.z`.
|
||||
|
||||
```ucm
|
||||
.> debug.numberedArgs
|
||||
|
||||
1. bar.z
|
||||
2. bar.z
|
||||
|
||||
```
|
||||
We can then delete the dependent term, and then delete `foo`.
|
||||
|
||||
```ucm
|
||||
.> delete.term 1
|
||||
|
||||
Done.
|
||||
|
||||
.> delete.namespace foo
|
||||
|
||||
Done.
|
||||
|
||||
```
|
Loading…
Reference in New Issue
Block a user