Matita HomeMatita HomeTable of Contents
notation usage "presentation" associativity with precedence p for content
notation [usage] "notation_lhs" [associativity] with precedence nat for notation_rhs
Declares a mapping between the presentation AST presentation and the content AST content. The declared presentation AST fragment presentation is at precedence level p. The precedence level is used to determine where parentheses must be inserted. In particular, the content AST fragment content is actually a pattern, since it contains placeholders (variables) for sub-ASTs. Every placeholder for a term is given an expected precedence level. Parentheses must be inserted around sub-ASTs having a precedence level strictly smaller than the expected one.
If presentation describes a binary infix operator and if no precedence level is explicitly given for the operator arguments, an associativity declaration can be given to automatically choose the right level for the operands. Otherwise, no associativity can be given.
If direction is omitted, the mapping is bi-directional and is used both during parsing and pretty-printing of terms. If direction is >, the mapping is used only during parsing; if it is <, it is used only during pretty-printing. Thus it is possible to use simple notations to type for writing the term, and nicer ones for rendering it.
Table 5.2. associativity
| associativity | ::= | left associative | Left associative |
| | | right associative | Right associative | |
| | | non associative | Non associative (default) |
Table 5.4. unparsed_ast
| unparsed_ast | ::= | @{enriched_term} | A content level AST (a term which is parsed, but not disambiguated). |
| | | @id | @id is just an abbreviation for @{id} | |
| | | @csymbol | @'symbol is just an abbreviation for @{'symbol} |
Table 5.5. enriched_term
| enriched_term | ::= | 〈〈A term that may contain occurrences of unparsed_meta, even as variable names in binders, and occurrences of csymbol〉〉 | TODO |
Table 5.6. unparsed_meta
| unparsed_meta | ::= | ${level2_meta} | TODO |
| | | $id | $id is just an abbreviation for ${id} | |
| | | $_ | $_ is just an abbreviation for ${_} |
Table 5.7. level2_meta
| level2_meta | ::= | unparsed_ast | TODO |
| | | term nat id | TODO | |
| | | number id | TODO | |
| | | ident id | TODO | |
| | | fresh id | TODO | |
| | | anonymous | TODO | |
| | | id | TODO | |
| | | fold [left|right] level2_meta rec id level2_meta | TODO | |
| | | default level2_meta level2_meta | TODO | |
| | | if level2_meta then level2_meta else level2_meta | TODO | |
| | | fail | TODO |
Table 5.9. layout
| layout | ::= | layout \sub layout | Subscript |
| | | layout \sup layout | Superscript | |
| | | layout \below layout | ||
| | | layout \above layout | ||
| | | layout \over layout | ||
| | | layout \atop layout | ||
| | | layout \frac layout | Fraction | |
| | | \infrule layout layout layout | Inference rule (premises, conclusion, rule name) | |
| | | \sqrt layout | Square root | |
| | | \root layout \of layout | Generalized root | |
| | | hbox ( layout [layout]… ) | Horizontal box | |
| | | vbox ( layout [layout]… ) | Vertical box | |
| | | hvbox ( layout [layout]… ) | Horizontal and vertical box | |
| | | hovbox ( layout [layout]… ) | Horizontal or vertical box | |
| | | break | Breakable space | |
| | | ( layout [layout]… ) | Group | |
| | | id | Placeholder for a term with no explicit precedence | |
| | | term nat id | Placeholder for a term with explicit expected precedence | |
| | | number id | Placeholder for a natural number | |
| | | ident id | Placeholder for an identifier | |
| | | literal | Literal | |
| | | opt layout | Optional layout (it can be omitted for parsing) | |
| | | list0 layout [sep literal] | List of layouts separated by sep (default: any blank) | |
| | | list1 layout [sep literal] | Non empty list of layouts separated by sep (default: any blank) | |
| | | mstyle id value (layout) | Style attributes like color #ff0000 | |
| | | mpadded id value (layout) | padding attributes like width -150% | |
| | | maction (layout) [ (layout) … ] | Alternative notations (output only) |