gospel 0.3.0 (latest) · OCaml Package

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 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

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

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

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

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

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

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

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

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

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

val 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

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

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

val t_true : 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 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

val 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

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

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

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

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

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

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

package gospel