package dolmen
package dolmen
-
dolmen
-
dolmen_intf
-
-
dolmen_line
-
dolmen_smtlib2
-
dolmen_smtlib2_v6
-
dolmen_std
-
-
dolmen_tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Minium required signature for tags to typecheck smtlib's core/base theory.
val named : string tA tag used to named formulas in smtlib. Should correspond to the `:named` attribute.
Multi-triggers (typically annotated on the body of a quantified formula and not the quantified formula itself). Each term is a multi-trigger represented as a conjunction of triggers.
val rwrt : unit tA flag (i.e. unit tag), indicating that the tagged term/formula is to be considered as a rewrite rule.