Matita HomeMatita Homeinterpretation "description" 'symbol p1 … pn =
rhs
interpretation qstring csymbol [interpretation_argument]… = interpretation_rhs
It declares a bi-directional mapping {…} between the content-level AST 'symbol t1 … tn and the semantic term rhs[{t1}/p1;…;{tn}/pn] (the simultaneous substitution in rhs of the interpretation {…} of every content-level actual argument ti for its corresponding formal parameter pi). The description must be a textual description of the meaning associated to 'symbol by this interpretation, and is used by the user interface of Matita to provide feedback on the interpretation of ambiguous terms.
Table 5.11. interpretation_argument
| interpretation_argument | ::= | [η.]… id | A formal parameter. If the name of the formal parameter is prefixed by n symbols "η", then the mapping performs (multiple) η-expansions to grant that the semantic actual parameter begins with at least n λ-abstractions. |
Table 5.12. interpretation_rhs
| interpretation_rhs | ::= | uri | A constant, specified by its URI |
| | | id | A constant, specified by its name, or a bound variable. If the constant name is ambiguous, the one corresponding to the last implicitly or explicitly specified alias is used. | |
| | | ? | An implicit parameter | |
| | | ( interpretation_rhs [interpretation_rhs]… ) | An application |