package gospel

  1. Overview
  2. Docs
module Ident = Identifier.Ident
type pattern = {
  1. p_node : pattern_node;
  2. p_ty : Ttypes.ty;
  3. p_loc : Ppxlib.Location.t;
}
and pattern_node =
  1. | Pwild
    (*

    _

    *)
  2. | Pvar of Symbols.vsymbol
    (*

    x

    *)
  3. | Papp of Symbols.lsymbol * pattern list
    (*

    Constructor

    *)
  4. | Por of pattern * pattern
    (*

    p1 | p2

    *)
  5. | Pas of pattern * Symbols.vsymbol
    (*

    p as vs

    *)
  6. | Pinterval of char * char
  7. | Pconst of Ppxlib.constant
val pp_pattern : Ppx_deriving_runtime.Format.formatter -> pattern -> Ppx_deriving_runtime.unit
val show_pattern : pattern -> Ppx_deriving_runtime.string
val pp_pattern_node : Ppx_deriving_runtime.Format.formatter -> pattern_node -> Ppx_deriving_runtime.unit
val show_pattern_node : pattern_node -> Ppx_deriving_runtime.string
type binop =
  1. | Tand
  2. | Tand_asym
  3. | Tor
  4. | Tor_asym
  5. | Timplies
  6. | Tiff
val pp_binop : Ppx_deriving_runtime.Format.formatter -> binop -> Ppx_deriving_runtime.unit
type quant =
  1. | Tforall
  2. | Texists
val pp_quant : Ppx_deriving_runtime.Format.formatter -> quant -> Ppx_deriving_runtime.unit
type term = {
  1. t_node : term_node;
  2. t_ty : Ttypes.ty option;
  3. t_attrs : string list;
  4. t_loc : Ppxlib.Location.t;
}
and term_node =
  1. | Tvar of Symbols.vsymbol
  2. | Tconst of Ppxlib.constant
  3. | Tapp of Symbols.lsymbol * term list
  4. | Tfield of term * Symbols.lsymbol
  5. | Tif of term * term * term
  6. | Tlet of Symbols.vsymbol * term * term
  7. | Tcase of term * (pattern * term option * term) list
  8. | Tquant of quant * Symbols.vsymbol list * term
  9. | Tlambda of pattern list * term
  10. | Tbinop of binop * term * term
  11. | Tnot of term
  12. | Told of term
  13. | Ttrue
  14. | Tfalse
val pp_term : Ppx_deriving_runtime.Format.formatter -> term -> Ppx_deriving_runtime.unit
val pp_term_node : Ppx_deriving_runtime.Format.formatter -> term_node -> Ppx_deriving_runtime.unit
val show_term_node : term_node -> Ppx_deriving_runtime.string
OCaml

Innovation. Community. Security.