Terms are reified as elements of the data type Term of terms, with the following signature
subsort Qid < Term .
subsort Term < TermList .
op {_}_ : Qid Qid -> Term .
op _[_] : Qid TermList -> Term .
op _,_ : TermList TermList -> TermList [assoc] .
op _:_ : Term Qid -> Term .
op _::_ : Term Qid -> Term .
op error* : -> Term .
The first declaration, making Qid a subsort of Term, is used to
represent variables by the corresponding quoted identifiers. Thus, the
variable N is represented by 'N. The operator
{_}_ is used for representing constants essentially as pairs,
with the first argument the constant, in quoted form, and the second argument
the sort of the constant, also in quoted form. For example, the constant 0 in the module NAT in Section 2.5.4 below is represented as {'0}'Nat. The operator _[_] corresponds to the recursive
construction of terms out of subterms, with the first argument the top
operator in quoted form, and the second argument the list of its subterms,
where list concatenation is denoted _,_. For example, the term
s s 0 + s 0 of sort Nat in module NAT is meta-represented as
Since terms in the module META-LEVEL can be meta-represented just as terms in any other module, as already mentioned when discussing the universal theory, the representation of terms can be iterated. For example, the meta-meta-representation |¯ |¯s 0¯| ¯| of the term s 0 in NAT is the term'_+_['s_['s_[{'0}'Nat]], 's_[{'0}'Nat]].
'_[_][{"s}'Qid,'{_}_[{"0}'Qid,{"Nat}'Qid]].
For the most part, the meta-representation of terms involving built-in operators proceeds as for any other term. For example, the application of the equality predicate _==_ in the term s s 0 == s 0 is represented as the term
But since we can think of membership predicates t:s not as unary predicates, one for each sort s, but as a binary predicate with the second argument varying over sorts, it is natural to meta-represent them in a uniform way by means of a binary constructor _:_ with the first argument the representation of the term, and the second the representation of the sort as a quoted identifier. For example, the membership predicate s 0 : Nat is represented as the term'_==_['s_['s_[{'0}'Nat]], 's_[{'0}'Nat]].
Similarly, there is also a binary constructor _::_ for meta-representing the "lazy" membership predicate that does not evaluate the term in question at all, but uses only the syntactic declarations in the module's order-sorted signature and the membership axioms to decide whether the least sort (see, e.g., [26]) of the unreduced term is smaller or equal to a given sort. The last declaration for the data type of terms is a constant error* to be used as an error element.'s_[{'0}'Nat] : 'Nat.