The right-hand-side term is a pattern . A definition applies to some term t if t is an instance of the rhs term. The display definition matcher has a notion of meta-variable different from that of Nuprl's usual matching routines; it has 3 kinds of meta-variable: meta-parameters
meta-bound-variables
and meta-terms
.
Meta-parameters and meta-bound-variables correspond to text slots on the
left-hand side of a definition, and meta-terms correspond to term slots.
The rhs
term is restricted to being a term whose subterms are either
constant terms (terms with no meta-variables) or meta-terms.
To enter a meta-term use the name mterm. To make meta-parameters
or meta-bound-variables, position a text cursor in the appropriate
parameter or bound variable slot and give the CYCLE-META-STATUSCYCLE-META-STATUS
(
C-M
) command. Display-meta-variables are readily recognized because
they have <> as delimiters
.
The rhs term can contain normal parameters, bound variables and variable terms. These must match exactly for a definition to be applicable.