gospel 0.3.0 (latest) · OCaml Package

val ty_of_lb_arg : Tast.lb_arg -> Ttypes.ty

val vs_of_lb_arg : Tast.lb_arg -> Symbols.vsymbol

val type_spec : 
  bool ->
  (Symbols.lsymbol * bool) list ->
  (Symbols.vsymbol * Tterm.term list) option ->
  string ->
  Ppxlib.Location.t ->
  Tast.type_spec

val label_declaration : 
  'a ->
  Tast.mutable_flag ->
  Ppxlib.Location.t ->
  Ppxlib.attributes ->
  'a Tast.label_declaration

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:Symbols.vsymbol ->
  Symbols.lsymbol ->
  bool ->
  Symbols.vsymbol list ->
  Tterm.term option ->
  Tast.fun_spec option ->
  Ppxlib.Location.t ->
  string ->
  Tast.function_

val mk_axiom : 
  Gospel.Ttypes.Ident.t ->
  Tterm.term ->
  Ppxlib.Location.t ->
  string ->
  Tast.axiom

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

val type_declaration : 
  Ttypes.tysymbol ->
  (Ttypes.tvsymbol * (Ppxlib.Asttypes.variance * Ppxlib.Asttypes.injectivity))
    list ->
  (Ttypes.ty * Ttypes.ty * Ppxlib.Location.t) list ->
  Tast.type_kind ->
  Tast.private_flag ->
  Ttypes.ty option ->
  Ppxlib.attributes ->
  Tast.type_spec option ->
  Ppxlib.Location.t ->
  Tast.type_declaration

val extension_constructor : 
  Gospel.Ttypes.Ident.t ->
  Ttypes.xsymbol ->
  Ppxlib.extension_constructor_kind ->
  Ppxlib.Location.t ->
  Ppxlib.attributes ->
  Tast.extension_constructor

val constructor_decl : 
  Symbols.lsymbol ->
  (Gospel.Ttypes.Ident.t * Ttypes.ty) Tast.label_declaration list ->
  Ppxlib.Location.t ->
  Ppxlib.attributes ->
  Tast.constructor_decl

val type_exception : 
  Tast.extension_constructor ->
  Ppxlib.Location.t ->
  Ppxlib.attributes ->
  Tast.type_exception

val mk_sig_item : 
  Tast.signature_item_desc ->
  Ppxlib.Location.t ->
  Tast.signature_item

package gospel