module UtilRepr (T : REPR) : sig .. end
type T.t
val head_sym : T.t -> TermInner.id
val to_seq : T.t -> (T.t -> 'a) -> unit
module VarSet: Var.Set(T)
val to_seq_free_vars : ?bound:VarSet.t ->
T.t -> (T.t TermInner.var -> unit) -> unit
val to_seq_consts : T.t -> TermInner.id Sequence.t
val free_vars : ?bound:VarSet.t -> T.t -> VarSet.t
val is_var : T.t -> bool
val is_const : T.t -> bool
val is_closed : T.t -> bool
val is_undefined : T.t -> bool
val to_seq_vars : T.t -> T.t TermInner.var Sequence.t
val free_meta_vars : ?init:T.t MetaVar.t ID.Map.t -> T.t -> T.t MetaVar.t ID.Map.t
val bind_unfold : TermInner.Binder.t -> T.t -> T.t TermInner.var list * T.t
val fun_unfold : T.t -> T.t TermInner.var list * T.t
val ty_unfold : T.t -> T.t TermInner.var list * T.t list * T.t
val ty_is_Type : T.t -> bool
val ty_is_Kind : T.t -> bool
val ty_is_Prop : T.t -> bool
val ty_is_unitype : T.t -> bool
val ty_returns : T.t -> T.t
val ty_returns_Type : T.t -> bool
val ty_returns_Prop : T.t -> bool
val get_ty_arg : T.t -> int -> T.t option
val ty_num_param : T.t -> int