Binder

Ltac2.Constr.Binder

type t = binder

type relevance = Sorts.relevance

val make : Environ.env -> Evd.evar_map -> Names.Name.t -> constr -> (t, unit) Stdlib.result

make env sigma name typ creates a binder given the name and the type of the bound variable. Fails if the type is not a type in the given environment.

val unsafe_make : Names.Name.t -> relevance -> constr -> t

unsafe_make name rel typ creates a binder given the name, relevance, and type of the bound variable.

val name : t -> Names.Name.t

name binder retrieves the name of the binder.

val type_ : t -> constr

type_ binder retrieves the type of the binder.

val relevance : t -> relevance

relevance binder retrieves the relevance of the binder.