Lines Matching refs:token
182 serie di token. Per maggiori informazioni sul lexing, si veda la Sezione~\ref{HOL-lex}.
210 differenti da qualsiasi token che appariva nell'input
229 \index{token!sopprimere il comportamento di parsing dei|(}
253 \index{token!sopprimere il comportamento di parsing dei|)}
401 il nome di una costante, o un token che appare in una regola di sintassi concreta
405 stesso di un token di una regola di sintassi concreta, allora il comportamento � di
407 usata come il token.
411 \index{token!Caratteri unicode}
417 caratteri. A meno che ci sia gi� nella grammatica uno specifico token ``misto'',
418 i token si dividono quando la classe di caratteri cambia. Cos�, nella
423 il lexer vedr� due token, \holtxt{++} e \holtxt{a}, perch�
429 permettere a stringhe come \holtxt{$\lambda$x.x} di essere divise dal lexer in \emph{quattro} token.)
754 Di fatto tuttavia, in un termine come $f(x)$, dove $f$ e $x$ non hanno fixity, la sintassi � trattata come se ci fosse una invisibile applicazione di funzione infissa tra i due token: $f\cdot{}x$.