package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
type location = ParseLocation.t
type builtin =
  1. | Wildcard
  2. | Ttype
  3. | Prop
  4. | True
  5. | False
  6. | Eq
  7. | Distinct
  8. | Ite
  9. | Sequent
  10. | Subtype
  11. | Product
  12. | Union
  13. | Not
  14. | And
  15. | Or
  16. | Nand
  17. | Xor
  18. | Nor
  19. | Imply
  20. | Implied
  21. | Equiv
type binder =
  1. | All
  2. | Ex
  3. | Pi
  4. | Arrow
  5. | Let
  6. | Fun
  7. | Choice
  8. | Description
type descr =
  1. | Symbol of Id.t
  2. | Builtin of builtin
  3. | Colon of t * t
  4. | App of t * t list
  5. | Binder of binder * t list * t
and t = {
  1. term : descr;
  2. attr : t list;
  3. loc : location option;
}
val eq_t : t
val neq_t : t
val wildcard : t
val tType : t
val prop : t
val true_ : t
val false_ : t
val not_t : t
val or_t : t
val and_t : t
val xor_t : t
val nor_t : t
val nand_t : t
val equiv_t : t
val implied_t : t
val implies_t : t
val data_t : t
val var : ?loc:location -> Id.t -> t
val const : ?loc:location -> Id.t -> t
val atom : ?loc:location -> int -> t
val distinct : ?loc:location -> Id.t -> t
val int : ?loc:location -> string -> t
val rat : ?loc:location -> string -> t
val real : ?loc:location -> string -> t
val hexa : ?loc:location -> string -> t
val binary : ?loc:location -> string -> t
val colon : ?loc:location -> t -> t -> t
val eq : ?loc:location -> t -> t -> t
val not_ : ?loc:location -> t -> t
val or_ : ?loc:location -> t list -> t
val and_ : ?loc:location -> t list -> t
val imply : ?loc:location -> t -> t -> t
val equiv : ?loc:location -> t -> t -> t
val apply : ?loc:location -> t -> t list -> t
val ite : ?loc:location -> t -> t -> t -> t
val pi : ?loc:location -> t list -> t -> t
val letin : ?loc:location -> t list -> t -> t
val forall : ?loc:location -> t list -> t -> t
val exists : ?loc:location -> t list -> t -> t
val lambda : ?loc:location -> t list -> t -> t
val choice : ?loc:location -> t list -> t -> t
val description : ?loc:location -> t list -> t -> t
val arrow : ?loc:location -> t -> t -> t
val product : ?loc:location -> t -> t -> t
val union : ?loc:location -> t -> t -> t
val subtype : ?loc:location -> t -> t -> t
val sequent : ?loc:location -> t list -> t list -> t
val annot : ?loc:location -> t -> t list -> t
val sexpr : ?loc:location -> t list -> t
val fun_ty : ?loc:location -> t list -> t -> t
val pp : Buffer.t -> t -> unit
val print : Format.formatter -> t -> unit