package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
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