package gospel

  1. Overview
  2. Docs
val ty_of_lb_arg : Tast.lb_arg -> Ttypes.ty
val vs_of_lb_arg : Tast.lb_arg -> Tterm.vsymbol
val type_spec : bool -> (Tterm.lsymbol * bool) list -> Tterm.term list -> string -> Ppxlib.Location.t -> Tast.type_spec
val mk_val_spec : Tast.lb_arg list -> Tast.lb_arg list -> Tterm.term list -> Tterm.term list -> Tterm.term list -> (Ttypes.xsymbol * (Tterm.pattern * Tterm.term) list) list -> Tterm.term list -> Tterm.term list -> bool -> bool -> string list -> string -> Ppxlib.Location.t -> Tast.val_spec
val mk_fun_spec : Tterm.term list -> Tterm.term list -> Tterm.term list -> bool -> string -> Ppxlib.Location.t -> Tast.fun_spec
val mk_function : ?result:Tterm.vsymbol -> Tterm.lsymbol -> bool -> Tterm.vsymbol list -> Tterm.term option -> Tast.fun_spec option -> Ppxlib.Location.t -> string -> Tast.function_
val mk_val_description : Gospel.Ttypes.Ident.t -> Ppxlib.core_type -> string list -> Ppxlib.attributes -> Tast.lb_arg list -> Tast.lb_arg list -> Tast.val_spec option -> Ppxlib.Location.t -> Tast.val_description
OCaml

Innovation. Community. Security.