package gospel

  1. Overview
  2. Docs
module Ident = Identifier.Ident
val t_free_vars : Tterm.term -> Symbols.Svs.t
val t_free_vs_in_set : Symbols.Svs.t -> Tterm.term -> unit
val t_prop : Tterm.term -> Tterm.term
val t_type : Tterm.term -> Ttypes.ty
val t_ty_check : Tterm.term -> Ttypes.ty option -> unit
val ls_arg_inst : Symbols.lsymbol -> Tterm.term list -> Ttypes.ty Ttypes.Mtv.t
val p_interval : char -> char -> Ppxlib.Location.t -> Tterm.pattern
val t_lambda : Tterm.pattern list -> Tterm.term -> Ttypes.ty option -> Ppxlib.Location.t -> Tterm.term
val t_false : Ppxlib.Location.t -> Tterm.term
val t_attr_set : string list -> Tterm.term -> Tterm.term
val t_bool_true : Ppxlib.Location.t -> Tterm.term
val t_bool_false : Ppxlib.Location.t -> Tterm.term
val f_forall : Symbols.vsymbol list -> Tterm.term -> Ttypes.ty option -> Ppxlib.Location.t -> Tterm.term
val f_exists : Symbols.vsymbol list -> Tterm.term -> Ttypes.ty option -> Ppxlib.Location.t -> Tterm.term
OCaml

Innovation. Community. Security.