Matita HomeMatita Homealias id "s" = "def"
alias symbol "s" (instance n) = "def"
alias num (instance n) = "def"
alias [id qstring = qstring | symbol qstring [(instance nat)] = qstring | num [(instance nat)] = qstring ]
Used to give an hint to the disambiguating parser. When the parser is faced to the identifier (or symbol) s or to any number, it will prefer interpretations that "map s (or the number) to def". For identifiers, "def" is the URI of the interpretation. E.g.: cic:/matita/nat/nat.ind#xpointer(1/1/1) for the first constructor of the first inductive type defined in the block of inductive type(s) cic:/matita/nat/nat.ind. For symbols and numbers, "def" is the label used to mark the wanted interpretation.
When a symbol or a number occurs several times in the term to be parsed, it is possible to give an hint only for the instance n. When the instance is omitted, the hint is valid for every occurrence.
Hints are automatically inserted in the script by Matita every time the user is interactively asked a question to disambiguate a term. This way the user won't be posed the same question twice when the script will be executed again.