1 %% commento segato dal lexer
3 (* commento che va nell'ast, ma non viene contato
4 come step perche' non e' un executable
7 alias num (instance 0) = "natural number".
8 alias symbol "eq" (instance 0) = "leibnitz's equality".
11 %% commento segato dal lexer
16 %% questo lo si vuole tenere anche dopo la hint
19 apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1).
21 (* commenti che non devono essere colorati perche'
22 non c'e' nulla di eseguibile dopo di loro