`Unsafe`#

Ltac2.Constr.Unsafe

Low-level access to kernel terms. Use with care!

val kind :
  Evd.evar_map ->
  t ->
  (t, t, EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t)
    Constr.kind_of_term

kind sigma t returns the kind view of t.

val make :
  (t, t, EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t)
    Constr.kind_of_term ->
  t

make kind constructs a term from the given kind.

val check : Environ.env -> Evd.evar_map -> t -> Evd.evar_map * t

check env sigma t checks that the term t generated by unsafe means is indeed safe in the current environment, and returns it along with the updated evar map.

Raises if the check fails.

val liftn : int -> int -> t -> t

liftn n k t lifts by n indices greater than or equal to k in t. Note that with respect to substitution calculi's terminology, n is the shift and k is the lift.

val substnl : EConstr.Vars.substl -> int -> t -> t

substnl [r₁; …; rₙ] k t substitutes in parallel Rel(k+1); …; Rel(k+n) with r₁; …; rₙ in t.

val closenl : Evd.evar_map -> ident list -> int -> t -> t

closenl sigma [x₁; …; xₙ] k t abstracts over variables x₁; …; xₙ and replaces them with Rel(k); …; Rel(k+n-1) in t. If two names are identical, the one of least index is kept.

val closedn : Evd.evar_map -> int -> t -> bool

closedn sigma n t is true iff t is a closed term under n binders.

val noccur_between : Evd.evar_map -> int -> int -> t -> bool

noccur_between sigma n m t returns true iff Rel p does not occur in term t for n <= p < n+m.

type case = Constr.case_info

val case : Environ.env -> inductive -> (case, unit) Stdlib.result

case env ind generates the case information for a given inductive type.

module Case : sig ... end

Unsafe#

`Unsafe`#