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.ty
val parse_term :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.term
val parse_statement_list :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.statement list
val parse_statement :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.UntypedAST.statement
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>