helm/www/matita/docs/manual-0.5.9/sec_usernotation.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 5. Extending the syntax</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="prev" href="tacticargs.html" title="Tactic arguments" /><link rel="next" href="ch05s02.html" title="interpretation" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 5. Extending the syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tacticargs.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="ch05s02.html">Next</a></td></tr></table><hr /></div><div class="chapter"><div class="titlepage"><div><div><h1 class="title"><a id="sec_usernotation"></a>Chapter 5. Extending the syntax</h1></div></div></div><div class="toc"><p><strong>Table of Contents</strong></p><dl class="toc"><dt><span class="sect1"><a href="sec_usernotation.html#idp70046384">notation</a></span></dt><dt><span class="sect1"><a href="ch05s02.html">interpretation</a></span></dt></dl></div>
   3   Introduction: <span class="emphasis"><em>TODO</em></span><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="idp70046384"></a>notation</h2></div></div></div><p><strong class="userinput"><code>notation usage "presentation" associativity with precedence p for content</code></strong></p><p><a id="notation"></a>
   4     </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p><span class="bold"><strong>notation</strong></span>
   5            [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.usage">usage</a></em></span>] <span class="bold"><strong>"</strong></span><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.notation_lhs">notation_lhs</a></em></span><span class="bold"><strong>"</strong></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.associativity">associativity</a></em></span>] <span class="bold"><strong>with</strong></span> <span class="bold"><strong>precedence</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>
   6            <span class="bold"><strong>for</strong></span>
   7            <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.notation_rhs">notation_rhs</a></em></span>
   8           </p></dd><dt><span class="term">Action:</span></dt><dd><p>Declares a mapping between the presentation
   9           AST <span class="command"><strong>presentation</strong></span> and the content AST
  10           <span class="command"><strong>content</strong></span>. The declared presentation AST fragment
  11           <span class="command"><strong>presentation</strong></span> is at precedence level
  12           <span class="command"><strong>p</strong></span>. The precedence level is used to determine where
  13           parentheses must be inserted. In particular, the content AST fragment
  14           <span class="command"><strong>content</strong></span> is actually a pattern, since it contains
  15           placeholders (variables) for sub-ASTs. Every placeholder for a term
  16           is given an expected precedence level. Parentheses must be inserted
  17           around sub-ASTs having a precedence level strictly smaller than the
  18           expected one.</p><p>If <span class="command"><strong>presentation</strong></span> describes a binary
  19           infix operator and if no precedence level is explicitly given for the
  20           operator arguments, an <span class="command"><strong>associativity</strong></span> declaration
  21           can be given to automatically choose the right level for the operands.
  22           Otherwise, no <span class="command"><strong>associativity</strong></span> can be given.</p><p>If <span class="command"><strong>direction</strong></span> is
  23           omitted, the mapping is bi-directional and is used both during
  24           parsing and pretty-printing of terms. If <span class="command"><strong>direction</strong></span>
  25           is <span class="command"><strong>&gt;</strong></span>, the mapping is used only during parsing;
  26           if it is <span class="command"><strong>&lt;</strong></span>, it is used only during
  27           pretty-printing. Thus it is possible to use simple notations to type
  28           for writing the term, and nicer ones for rendering it.</p></dd><dt><span class="term">Notation arguments:</span></dt><dd><div class="table"><a id="idp70117712"></a><p class="title"><strong>Table 5.1. usage</strong></p><div class="table-contents"><table summary="usage" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.usage"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.usage">usage</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>&lt;</strong></span></td><td style="">Only for pretty-printing</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>&gt;</strong></span></td><td style="">Only for parsing</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70126480"></a><p class="title"><strong>Table 5.2. associativity</strong></p><div class="table-contents"><table summary="associativity" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.associativity"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.associativity">associativity</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>left</strong></span> <span class="bold"><strong>associative</strong></span></td><td style="">Left associative</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>right</strong></span> <span class="bold"><strong>associative</strong></span></td><td style="">Right associative</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>non</strong></span> <span class="bold"><strong>associative</strong></span></td><td style="">Non associative (default)</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70139344"></a><p class="title"><strong>Table 5.3. notation_rhs</strong></p><div class="table-contents"><table summary="notation_rhs" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.notation_rhs"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.notation_rhs">notation_rhs</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_ast">unparsed_ast</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_meta">unparsed_meta</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70148064"></a><p class="title"><strong>Table 5.4. unparsed_ast</strong></p><div class="table-contents"><table summary="unparsed_ast" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.unparsed_ast"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_ast">unparsed_ast</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>@{</strong></span><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.enriched_term">enriched_term</a></em></span><span class="bold"><strong>}</strong></span></td><td style="">A content level AST (a term which is parsed, but not disambiguated).</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>@</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="command"><strong>@id</strong></span> is just an abbreviation for <span class="command"><strong>@{id}</strong></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>@</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.csymbol">csymbol</a></em></span></td><td style=""><span class="command"><strong>@'symbol</strong></span> is just an abbreviation for <span class="command"><strong>@{'symbol}</strong></span></td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70166064"></a><p class="title"><strong>Table 5.5. enriched_term</strong></p><div class="table-contents"><table summary="enriched_term" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.enriched_term"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.enriched_term">enriched_term</a></em></span></td><td style="">::=</td><td style="">〈〈A term that may contain occurrences of <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_meta">unparsed_meta</a></em></span>, even as variable names in binders, and occurrences of <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.csymbol">csymbol</a></em></span>〉〉</td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70173616"></a><p class="title"><strong>Table 5.6. unparsed_meta</strong></p><div class="table-contents"><table summary="unparsed_meta" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.unparsed_meta"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_meta">unparsed_meta</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>${</strong></span><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span><span class="bold"><strong>}</strong></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>$</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="command"><strong>$id</strong></span> is just an abbreviation for <span class="command"><strong>${id}</strong></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>$</strong></span><span class="bold"><strong>_</strong></span></td><td style=""><span class="command"><strong>$_</strong></span> is just an abbreviation for <span class="command"><strong>${_}</strong></span></td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70190032"></a><p class="title"><strong>Table 5.7. level2_meta</strong></p><div class="table-contents"><table summary="level2_meta" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.level2_meta"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.unparsed_ast">unparsed_ast</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>term</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>number</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>ident</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>fresh</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>anonymous</strong></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>fold</strong></span> [<span class="bold"><strong>left</strong></span>|<span class="bold"><strong>right</strong></span>] <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span> <span class="bold"><strong>rec</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>default</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>if</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span> <span class="bold"><strong>then</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span> <span class="bold"><strong>else</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.level2_meta">level2_meta</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>fail</strong></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70234960"></a><p class="title"><strong>Table 5.8. notation_lhs</strong></p><div class="table-contents"><table summary="notation_lhs" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.notation_lhs"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.notation_lhs">notation_lhs</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]…</td><td class="auto-generated" style=""> </td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70242480"></a><p class="title"><strong>Table 5.9. layout</strong></p><div class="table-contents"><table summary="layout" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.layout"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\sub</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Subscript</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\sup</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Superscript</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\below</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style=""> </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\above</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style=""> </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\over</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style=""> </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\atop</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style=""> </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\frac</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Fraction</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>\infrule</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Inference rule (premises, conclusion, rule name)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>\sqrt</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Square root</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>\root</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> <span class="bold"><strong>\of</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Generalized root</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>hbox</strong></span> <span class="bold"><strong>(</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]… <span class="bold"><strong>)</strong></span></td><td style="">Horizontal box</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>vbox</strong></span> <span class="bold"><strong>(</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]… <span class="bold"><strong>)</strong></span></td><td style="">Vertical box</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>hvbox</strong></span> <span class="bold"><strong>(</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]… <span class="bold"><strong>)</strong></span></td><td style="">Horizontal and vertical box</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>hovbox</strong></span> <span class="bold"><strong>(</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]… <span class="bold"><strong>)</strong></span></td><td style="">Horizontal or vertical box</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>break</strong></span></td><td style="">Breakable space</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>(</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>]… <span class="bold"><strong>)</strong></span></td><td style="">Group</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">Placeholder for a term with no explicit precedence</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>term</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">Placeholder for a term with explicit expected precedence</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>number</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">Placeholder for a natural number</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>ident</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">Placeholder for an identifier</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.literal">literal</a></em></span></td><td style="">Literal</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>opt</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span></td><td style="">Optional layout (it can be omitted for parsing)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>list0</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>
  29                [<span class="bold"><strong>sep</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.literal">literal</a></em></span>]</td><td style="">List of layouts separated by <span class="command"><strong>sep</strong></span> (default:
  30                any blank)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>list1</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>
  31                [<span class="bold"><strong>sep</strong></span> <span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.literal">literal</a></em></span>]</td><td style="">Non empty list of layouts separated by <span class="command"><strong>sep</strong></span>
  32                (default: any blank)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>mstyle</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> value (<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>)
  33         </td><td style="">Style attributes like color #ff0000</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>mpadded</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span> value (<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>)
  34         </td><td style="">padding attributes like width -150%</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>maction</strong></span> (<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>)
  35                 [ (<span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.layout">layout</a></em></span>) … ]
  36         </td><td style="">Alternative notations (output only)</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp70356272"></a><p class="title"><strong>Table 5.10. literal</strong></p><div class="table-contents"><table summary="literal" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.literal"></a><span class="emphasis"><em><a class="link" href="sec_usernotation.html#grammar.literal">literal</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.symbol">symbol</a></em></span></td><td style="">Unicode symbol</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></td><td style="">Natural number (a constant)</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>'</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span><span class="bold"><strong>'</strong></span></td><td style="">New keyword for the lexer</td></tr></tbody></table></div></div><br class="table-break" /></dd></dl></div><p>
  37   </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tacticargs.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="ch05s02.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Tactic arguments </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> interpretation</td></tr></table></div></body></html>