Matitaweb:

Matitaweb:

Improved support for notations enriched with hyperlinks.
This revision introduces a "ref" keyword which can be used in the lefthand side
of notation statements. "ref" can only be used to decorate literals (i.e.
symbols, numbers, or keywords). The syntax is as follows:

  LITERAL ::= SIMPLE_LITERAL
           |  ref CSYMBOL SIMPLE_LITERAL

For example, the notation

  ref 'cons [ list0 x sep ; ref 'nil ]

used as the compact notation for lists specifies that the `[' symbol will be
enriched with the interpretation of 'cons nodes of the AST, and the `]' symbol
with the interpretation of 'nil nodes of the AST.