add

myProject/main> add
myProject/main> add myNewTerm

Adds all the definitions from the most recently typechecked file to the codebase.

FAQ about the add command

I got an error about "these definitions failed" on add

This message happens when some of the definitions couldn't be added to the codebase. Most commonly this is because you are trying to add a term that already exists in the codebase with the same namespace and name.

x These definitions failed:

Reason
needs update   myFunction : Doc

Entering update instead of add will turn this failure into a successful update.