25 lines
778 B
OCaml
25 lines
778 B
OCaml
{
|
|
open Parser
|
|
}
|
|
|
|
rule token_ty = parse
|
|
| [' ' '\t' '\n'] { token_ty lexbuf }
|
|
| eof { EOF }
|
|
|
|
| '(' { LPAREN }
|
|
| ')' { RPAREN }
|
|
| "->" { RARROW }
|
|
| '~' { TILDE }
|
|
| "False" { FALSE }
|
|
| ['A'-'Z']+['0'-'9']* as s { TYPE_NAME s }
|
|
|
|
and token_tactic = parse
|
|
| [' ' '\t' '\n'] { token_tactic lexbuf }
|
|
| eof { EOF }
|
|
| "intro" { INTRO }
|
|
| "assumption" { ASSUMPTION }
|
|
| "apply" { APPLY }
|
|
| "elim" { ELIM }
|
|
| ['a'-'z']+['0'-'9']* as s { VAR_NAME s }
|
|
| '.' { DOT }
|