{
    open Parser
}

rule token = parse
  | [' ' '\t' '\n']             { token lexbuf }
  | eof                         { EOF }

  | '('                         { LPAREN }
  | ')'                         { RPAREN }
  | "->"                        { RARROW }
  | '~'                         { TILDE }
  | "/\\"                       { LAND } (* logical and *)
  | "\\/"                       { LOR } (* logical or *)
  | ','                         { COMMA }

  | "intro"                     { INTRO }
  | "intros"                    { INTROS }
  | "assumption"                { ASSUMPTION }
  | "apply"                     { APPLY }
  | "elim"                      { ELIM }
  | "cut"                       { CUT }
  | "split"                     { SPLIT }
  | "left"                      { LEFT }
  | "right"                     { RIGHT }
  | "exact"                     { EXACT }

  | "False"                     { FALSE }
  | "True"                      { TRUE }

  | "fun"                       { FUN }
  | "=>"                        { MAPS_TO }
  | ':'                         { COLON }
  | "exf"                       { EXF }
  | "fst"                       { FST }
  | "snd"                       { SND }
  | "ig"                        { IG }
  | "id"                        { ID }
  | "case"                      { CASE }
  | 'I'                         { I }

  | '&'                         { AMPERSAND }

  | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
  | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
  | '.'                         { DOT }