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) |
+