sig
  type token =
      WILDCARD
    | VERTICAL_BAR
    | VAL
    | UPPER_WORD of string
    | TYPE
    | RIGHT_PAREN
    | RIGHT_BRACKET
    | REWRITE
    | QUOTED of string
    | PROP
    | PI
    | NAME
    | LOWER_WORD of string
    | LOGIC_TRUE
    | LOGIC_OR
    | LOGIC_NOT
    | LOGIC_NEQ
    | LOGIC_IMPLY
    | LOGIC_FORALL
    | LOGIC_FALSE
    | LOGIC_EXISTS
    | LOGIC_EQUIV
    | LOGIC_EQ
    | LOGIC_AND
    | LEMMA
    | LEFT_PAREN
    | LEFT_BRACKET
    | INCLUDE
    | GOAL
    | EQDEF
    | EOI
    | DOT
    | DEF
    | DATA
    | COMMA
    | COLON
    | ASSERT
    | ARROW
    | AND
    | AC
  exception Error
  val parse_ty :
    (Lexing.lexbuf -> Parse_zf.token) ->
    Lexing.lexbuf -> Libzipperposition.UntypedAST.ty
  val parse_term :
    (Lexing.lexbuf -> Parse_zf.token) ->
    Lexing.lexbuf -> Libzipperposition.UntypedAST.term
  val parse_statement_list :
    (Lexing.lexbuf -> Parse_zf.token) ->
    Lexing.lexbuf -> Libzipperposition.UntypedAST.statement list
  val parse_statement :
    (Lexing.lexbuf -> Parse_zf.token) ->
    Lexing.lexbuf -> Libzipperposition.UntypedAST.statement
end