Module `Gospel.Tterm_helper`Source

Sourcemodule Ident = Identifier.Ident

Sourceval t_free_vars : Tterm.term -> Symbols.Svs.t

Sourceval t_free_vs_in_set : Symbols.Svs.t -> Tterm.term -> unit

Sourceval t_prop : Tterm.term -> Tterm.term

Sourceval t_type : Tterm.term -> Ttypes.ty

Sourceval t_ty_check : Tterm.term -> Ttypes.ty option -> unit

Sourceval ls_arg_inst : Symbols.lsymbol -> Tterm.term list -> Ttypes.ty Ttypes.Mtv.t

val ls_app_inst : 
  Symbols.lsymbol ->
  Tterm.term list ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  Ttypes.ty Ttypes.Mtv.t

val mk_pattern : 
  Tterm.pattern_node ->
  Ttypes.ty ->
  Ppxlib.Location.t ->
  Tterm.pattern

Sourceval p_wild : Ttypes.ty -> Ppxlib.Location.t -> Tterm.pattern

Sourceval p_var : Symbols.vsymbol -> Ppxlib.Location.t -> Tterm.pattern

val p_app : 
  Symbols.lsymbol ->
  Tterm.pattern list ->
  Ttypes.ty ->
  Ppxlib.Location.t ->
  Tterm.pattern

Sourceval p_or : Tterm.pattern -> Tterm.pattern -> Ppxlib.Location.t -> Tterm.pattern

val p_as : 
  Tterm.pattern ->
  Symbols.vsymbol ->
  Ppxlib.Location.t ->
  Tterm.pattern

Sourceval p_interval : char -> char -> Ppxlib.Location.t -> Tterm.pattern

Sourceval p_const : Ppxlib.Parsetree.constant -> Ppxlib.Location.t -> Tterm.pattern

val mk_term : 
  Tterm.term_node ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  Tterm.term

Sourceval t_var : Symbols.vsymbol -> Ppxlib.Location.t -> Tterm.term

Sourceval t_const : Ppxlib.constant -> Ttypes.ty -> Ppxlib.Location.t -> Tterm.term

val t_app : 
  Symbols.lsymbol ->
  Tterm.term list ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  Tterm.term

val t_field : 
  Tterm.term ->
  Symbols.lsymbol ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  Tterm.term

val t_if : 
  Tterm.term ->
  Tterm.term ->
  Tterm.term ->
  Ppxlib.Location.t ->
  Tterm.term

val t_let : 
  Symbols.vsymbol ->
  Tterm.term ->
  Tterm.term ->
  Ppxlib.Location.t ->
  Tterm.term

val t_case : 
  Tterm.term ->
  (Tterm.pattern * Tterm.term option * Tterm.term) list ->
  Ppxlib.Location.t ->
  Tterm.term

val t_lambda : 
  Tterm.pattern list ->
  Tterm.term ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  Tterm.term

val t_binop : 
  Tterm.binop ->
  Tterm.term ->
  Tterm.term ->
  Ppxlib.Location.t ->
  Tterm.term

Sourceval t_not : Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval t_old : Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval t_true : Ppxlib.Location.t -> Tterm.term

Sourceval t_false : Ppxlib.Location.t -> Tterm.term

Sourceval t_attr_set : string list -> Tterm.term -> Tterm.term

Sourceval t_bool_true : Ppxlib.Location.t -> Tterm.term

Sourceval t_bool_false : Ppxlib.Location.t -> Tterm.term

Sourceval t_equ : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

val t_neq : 
  Tterm.term ->
  Tterm.term ->
  Ppxlib.Location.t ->
  Ppxlib.Location.t ->
  Tterm.term

val f_binop : 
  Tterm.binop ->
  Tterm.term ->
  Tterm.term ->
  Ppxlib.Location.t ->
  Tterm.term

Sourceval f_not : Tterm.term -> Ppxlib.Location.t -> Tterm.term

val t_quant : 
  Tterm.quant ->
  Symbols.vsymbol list ->
  Tterm.term ->
  Ttypes.ty option ->
  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

Sourceval f_and : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval f_and_asym : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval f_or : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval f_or_asym : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval f_implies : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

Sourceval f_iff : Tterm.term -> Tterm.term -> Ppxlib.Location.t -> Tterm.term

package gospel