2024-06-03 20:56:33 +03:00
|
|
|
```ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> builtins.merge
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
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
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
bar.z : Nat
|
|
|
|
foo.x : Nat
|
|
|
|
foo.y : Nat
|
|
|
|
|
|
|
|
```
|
|
|
|
Let's see what we have created...
|
|
|
|
|
|
|
|
```ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> ls
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
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
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> delete.namespace foo
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
⚠️
|
|
|
|
|
|
|
|
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
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> debug.numberedArgs
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
1. bar.z
|
|
|
|
2. bar.z
|
|
|
|
|
|
|
|
```
|
|
|
|
We can then delete the dependent term, and then delete `foo`.
|
|
|
|
|
|
|
|
```ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> delete.term 1
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
Done.
|
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> delete.namespace foo
|
2024-06-03 20:56:33 +03:00
|
|
|
|
|
|
|
Done.
|
|
|
|
|
|
|
|
```
|