New Term Entry

The term editor recognizes certain input sequences as indicating that a new term should be created. A new term structure can be created as follows:

• Position a term cursor and an empty slot.
• Enter the letters of the new term's opid
• Enter a (possibly empty) list of single letters, designating the new term's parameter types. The list should be delimited by { and } characters, and elements should be seperated by ,

  characters. Empty lists of parameter types are optional.

• Enter a (possibly empty) list of numbers, designating the number of binding variables for each subterm. The list should be delimited by ( and ) characters, and elements should be seperated by ; characters. This list specifying the arity of the term must be entered, even when it is empty.

For example, if you enter

the term myid{[natural]:n, [token]:t}([term]; [binding].[term])

is created.