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