.> add myNewTerm
Adds all the definitions from the most recently typechecked file to the codebase.
FAQ about theaddcommand
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. UCM shows a table of definitions along with the reason why they didn't succeed, like this:
x These definitions failed: Reason needs update myFunction : Doc
Here's what these reasons mean:
- needs update:The scratch file has a definition with the same name as an existing definition. Doing
updateinstead of add will turn this failure into a successful update.
- conflicted:The file has a definition whose name is currently conflicted. Resolving the conflict and then trying an update again will turn this into a successful update.
- term/ctor collision:A definition with the same name as an existing constructor for some data type. Rename your definition or the data type before trying again to
- ctor/term collision:A type defined in the file has a constructor that's named the same as an existing term. Rename that term or your constructor before trying again to
- needs alias:A definition in the file already has another name. You can use the
alias.typecommands to create new names for existing definitions.
- blocked:This definition couldn't be added because it dependended on another definition in the file that had a failed status.
- extra dependency:This definition was added because it was a dependency of a definition explicitly selected.
I want to undo a partially completed add where some of the definitions failed
You can use the
undocommand in the case of an undesired partially completed add.