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.
type constant = Ast.Term.constantDe 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.termtype view = private | Const of int| Lam of term| App of int * term * term list| Cons of term * term| Nil| Builtin of builtin * term list| CData of RawOpaqueData.t| UnifVar of FlexibleData.Elpi.t * term listTerms 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 mkBound : int -> termSmart constructors
val mkNil : termval mkDiscard : termval mkCData : RawOpaqueData.t -> termval mkUnifVar : FlexibleData.Elpi.t -> args:term list -> State.t -> termval mkConst : int -> termno check, works for globals and bound
val isApp : depth:int -> term -> booltype hyps = hyp listval constraints : Data.constraints -> suspended_goal listval no_constraints : Data.constraintsmodule Constants : sig ... endval set_extra_goals_postprocessing :
?descriptor:Setup.hoas_descriptor ->
(Conversion.extra_goals -> State.t -> State.t * Conversion.extra_goals) ->
unitval new_hoas_descriptor : unit -> Setup.hoas_descriptor