package logtk
Core types and algorithms for logic
Install
dune-project
Dependency
Authors
Maintainers
Sources
2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63
doc/logtk.parsers/Logtk_parsers/Parse_zf/index.html
Module Logtk_parsers.Parse_zf
type token = | WITH| WILDCARD| WHERE| VERTICAL_BAR| VAL| UPPER_WORD of string| TYPE| THEN| SINGLE_QUOTED of string| SEMI_COLON| RIGHT_PAREN| RIGHT_BRACKET| REWRITE| QUOTED of string| PROP| PI| MATCH| 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| LET| LEMMA| LEFT_PAREN| LEFT_BRACKET| INTEGER of string| INT| INCLUDE| IN| IF| GOAL| FUN| EQDEF| EOI| END| ELSE| DOT| DEF| DATA| COMMA| COLON| ASSERT| ARROW| ARITH_PRODUCT| ARITH_PLUS| ARITH_MINUS| ARITH_LT| ARITH_LEQ| ARITH_GT| ARITH_GEQ| AND
val parse_ty : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logtk.UntypedAST.tyval parse_term :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.termval parse_statement_list :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.statement listval parse_statement :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.statement