Module Parse_zf

module Parse_zf: sig .. end

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 -> token) ->
Lexing.lexbuf -> Libzipperposition.UntypedAST.ty
val parse_term : (Lexing.lexbuf -> token) ->
Lexing.lexbuf -> Libzipperposition.UntypedAST.term
val parse_statement_list : (Lexing.lexbuf -> token) ->
Lexing.lexbuf -> Libzipperposition.UntypedAST.statement list
val parse_statement : (Lexing.lexbuf -> token) ->
Lexing.lexbuf -> Libzipperposition.UntypedAST.statement