The theory DEFAULT is slightly more complex than TRIV, in that in addition to a sort it also requires that there be a distinguished ``default'' element in such a sort. Notice that DEFAULT imports TRIV in the following presentation:
fth DEFAULT is
including TRIV .
op 0 : -> Elt .
endfth
The inclusion of the theory TRIV into the theory DEFAULT is made explicit by the following view, whose name coincides with the name of the target theory.
view DEFAULT from TRIV to DEFAULT is endv
The Maude library also includes several views that map from DEFAULT to the various built-in data type modules by selecting the main sort and a distinguished element in it. In the case of the number sorts, this element is the zero, while for strings it is the empty string and for quoted identifiers is just the quote. Notice that operator mappings that are the identity (i.e., of the form op 0 to 0) do not appear explicitly in the following views but are left implicit. These views are named by appending ``0'' to the name of the selected sort; for example, the standard view from DEFAULT into RAT selecting the sort Rat and 0 as the default element is named Rat0.
view Nat0 from DEFAULT to NAT is
sort Elt to Nat .
endv
view Int0 from DEFAULT to INT is
sort Elt to Int .
endv
view Rat0 from DEFAULT to RAT is
sort Elt to Rat .
endv
view Float0 from DEFAULT to FLOAT is
sort Elt to Float .
op 0 to term 0.0 .
endv
view String0 from DEFAULT to STRING is
sort Elt to String .
op 0 to term "" .
endv
view Qid0 from DEFAULT to QID is
sort Elt to Qid .
op 0 to term ' .
endv