.> add
.> 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:

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. Doingupdateinstead 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 toaddorupdate.
  • 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 toaddorupdate.
  • needs alias:A definition in the file already has another name. You can use thealias.termoralias.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 theundocommand in the case of an undesired partially completed add.