package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = Term.t
type location = ParseLocation.t
type inductive = {
  1. id : Id.t;
  2. vars : term list;
  3. cstrs : (Id.t * term list) list;
  4. loc : location option;
}
type descr =
  1. | Pack of t list
  2. | Pop of int
  3. | Push of int
  4. | Prove
  5. | Consequent of term
  6. | Antecedent of term
  7. | Include of string
  8. | Set_logic of string
  9. | Get_info of string
  10. | Set_info of string * term option
  11. | Get_option of string
  12. | Set_option of string * term option
  13. | Def of Id.t * term
  14. | Decl of Id.t * term
  15. | Inductive of inductive
  16. | Get_proof
  17. | Get_unsat_core
  18. | Get_value of term list
  19. | Get_assignment
  20. | Get_assertions
  21. | Exit
and t = {
  1. id : Id.t;
  2. descr : descr;
  3. attr : term option;
  4. loc : location option;
}
val annot : ?loc:location -> term -> term list -> term
val include_ : ?loc:location -> string -> Id.t list -> t
val clause : ?loc:location -> term list -> t
val pop : ?loc:location -> int -> t
val push : ?loc:location -> int -> t
val assert_ : ?loc:location -> term -> t
val check_sat : ?loc:location -> unit -> t
val set_logic : ?loc:location -> string -> t
val get_info : ?loc:location -> string -> t
val set_info : ?loc:location -> (string * term option) -> t
val get_option : ?loc:location -> string -> t
val set_option : ?loc:location -> (string * term option) -> t
val type_decl : ?loc:location -> Id.t -> int -> t
val type_def : ?loc:location -> Id.t -> Id.t list -> term -> t
val fun_decl : ?loc:location -> Id.t -> term list -> term -> t
val fun_def : ?loc:location -> Id.t -> term list -> term -> term -> t
val get_proof : ?loc:location -> unit -> t
val get_unsat_core : ?loc:location -> unit -> t
val get_value : ?loc:location -> term list -> t
val get_assignment : ?loc:location -> unit -> t
val get_assertions : ?loc:location -> unit -> t
val exit : ?loc:location -> unit -> t
val tpi : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val thf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val tff : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val fof : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val cnf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val inductive : ?loc:location -> Id.t -> term list -> (Id.t * term list) list -> t
val data : ?loc:location -> t list -> t
val decl : ?loc:location -> Id.t -> term -> t
val definition : ?loc:location -> Id.t -> term -> term -> t
val goal : ?loc:location -> ?attr:term -> term -> t
val assume : ?loc:location -> ?attr:term -> term -> t
val rewrite : ?loc:location -> ?attr:term -> term -> t
val pp : Buffer.t -> t -> unit
val print : Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct