equal
deleted
inserted
replaced
26 |
26 |
27 The type constructor \texttt{gterm} can be generalized to a function |
27 The type constructor \texttt{gterm} can be generalized to a function |
28 over sets. It returns |
28 over sets. It returns |
29 the set of ground terms that can be formed over a set \isa{F} of function symbols. For |
29 the set of ground terms that can be formed over a set \isa{F} of function symbols. For |
30 example, we could consider the set of ground terms formed from the finite |
30 example, we could consider the set of ground terms formed from the finite |
31 set {\isa{\{Number 2, UnaryMinus, Plus\}}}. |
31 set \isa{\isacharbraceleft Number 2, UnaryMinus, |
|
32 Plus\isacharbraceright}. |
32 |
33 |
33 This concept is inductive. If we have a list \isa{args} of ground terms |
34 This concept is inductive. If we have a list \isa{args} of ground terms |
34 over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we |
35 over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we |
35 can apply \isa{f} to \isa{args} to obtain another ground term. |
36 can apply \isa{f} to \isa{args} to obtain another ground term. |
36 The only difficulty is that the argument list may be of any length. Hitherto, |
37 The only difficulty is that the argument list may be of any length. Hitherto, |