interpretation "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.

Interpretation arguments:

Table 5.11. interpretation_argument

interpretation_argument::=[η.]… idA 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::=uriA constant, specified by its URI
 |idA 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