This module exposes the low level representation of terms. * * The data type term is opaque and can only be accessed by using the * look API that exposes a term view. The look view automatically * substitutes assigned unification variables by their value.
De Bruijn levels (not indexes): the distance of the binder from the root. Starts at 0 and grows for bound variables; global constants have negative values.
De Bruijn levels (not indexes): the distance of the binder from the root. Starts at 0 and grows for bound variables; global constants have negative values.
type term = Data.termTerms must be inspected after dereferencing their head. If the resulting term is UVar then its uvar_body is such that get_assignment uvar_body = None
val mkGlobalS : string -> termSmart constructors
val mkNil : termval mkDiscard : termval mkCData : RawOpaqueData.t -> termval mkUnifVar : FlexibleData.Elpi.t -> args:term list -> State.t -> termtype hyps = hyp listval constraints : Data.constraints -> suspended_goal listval no_constraints : Data.constraintsmodule Constants : sig ... end