Delete

.> builtins.merge

The delete command can delete both terms and types.

First, let's make sure it complains when we try to delete a name that doesn't exist.

.> delete foo

Now for some easy cases. Deleting an unambiguous term, then deleting an unambiguous type.

foo = 1
structural type Foo = Foo Nat

.> add
.> delete foo
.> delete Foo
.> delete Foo.Foo

How about an ambiguous term?

foo = 1

.a> add

foo = 2

.b> add
.a> merge .b

A delete should remove both versions of the term.

.a> delete foo

.a> ls

Let's repeat all that on a type, for completeness.

structural type Foo = Foo Nat

.a> add

structural type Foo = Foo Boolean

.b> add
.a> merge .b

.a> delete Foo

.a> delete Foo.Foo

Finally, let's try to delete a term and a type with the same name.

foo = 1
structural type foo = Foo Nat

.> add

.> delete foo