module Cfg = Configmodule Ident = Gospel.Identifier.Identval constant_test : Gospel.Tast.val_description -> unit Reserr.reserrval no_functional_arg_or_returned_tuple :
Gospel.Tast.val_description ->
unit Reserr.reserrval is_a_function : Ppxlib.core_type -> boolval unify :
[< `Type of Gospel.Tast.type_declaration | `Value of string ] ->
Astlib.Ast_414.Parsetree.core_type ->
Ppxlib.core_type ->
(string * Ppxlib.core_type) list Reserr.reserrval ty_var_substitution :
Cfg.t ->
Gospel.Tast.val_description ->
(string * Ppxlib.core_type) list Reserr.reserrval split_args :
Cfg.t ->
Gospel.Tast.val_description ->
Gospel.Tast.lb_arg list ->
(Gospel.Symbols.Ident.t
* (Ppxlib.core_type * Gospel.Symbols.Ident.t option) list)
Reserr.reserrval get_state_description_with_index :
(Gospel.Symbols.vsymbol -> bool) ->
(Gospel.Tterm.Ident.t * 'a) list ->
Gospel.Tast.val_spec ->
(int * Ir.new_state_formulae) listval next_state :
Gospel.Symbols.Ident.t ->
(Gospel.Tterm.Ident.t * 'a) list ->
Gospel.Tast.val_spec ->
Ir.next_state Reserr.reserrval returned_value_description :
Gospel.Tast.val_spec ->
Gospel.Symbols.Ident.t ->
Ir.term listval postcond : Gospel.Tast.val_spec -> Ir.postcondval val_desc :
Cfg.t ->
(Gospel.Tterm.Ident.t * 'a) list ->
Gospel.Tast.val_description ->
Ir.value Reserr.reserrval sig_item :
Cfg.t ->
string ->
(Gospel.Tterm.Ident.t * 'a) list ->
Gospel.Tast.signature_item ->
Ir.value Reserr.reserr optionval state_and_invariants :
Cfg.t ->
Gospel.Tast.signature_item list ->
((Gospel.Symbols.Ident.t * Ppxlib.core_type) list
* (Gospel.Symbols.Ident.t * Ir.term list) option)
Reserr.reserrval init_state :
Cfg.t ->
(Gospel.Symbols.Ident.t * 'a) list ->
Gospel.Tast.signature_item list ->
(string * Ir.init_state) Reserr.reserrval signature :
Cfg.t ->
string ->
(Gospel.Tterm.Ident.t * 'a) list ->
Gospel.Tast.signature_item list ->
Ir.value list Reserr.reserrval ghost_functions :
Gospel.Tast.signature_item list ->
Gospel.Tast.function_ listval run : Gospel.Tast.signature_item list -> Cfg.t -> Ir.t Reserr.reserr