Module Constrexpr_ops

val sort_name_expr_eq : Constrexpr.sort_name_expr -> Constrexpr.sort_name_expr -> bool
val univ_level_expr_eq : Constrexpr.univ_level_expr -> Constrexpr.univ_level_expr -> bool
val sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> bool
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool

Equality on explicitation.

val constr_expr_eq_gen : (Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool) -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool
val constr_expr_eq : Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool

Equality on constr_expr. This is a syntactical one, which is oblivious to some parsing details, including locations.

val local_binder_eq : Constrexpr.local_binder_expr -> Constrexpr.local_binder_expr -> bool

Equality on local_binder_expr. Same properties as constr_expr_eq.

val binder_kind_eq : Constrexpr.binder_kind -> Constrexpr.binder_kind -> bool

Equality on binder_kind

Retrieving locations
val constr_loc : Constrexpr.constr_expr -> Loc.t option
val cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t option
val local_binders_loc : Constrexpr.local_binder_expr list -> Loc.t option
Constructors
Term constructors
val mkIdentC : Names.Id.t -> Constrexpr.constr_expr
val mkRefC : Libnames.qualid -> Constrexpr.constr_expr
val mkCastC : (Constrexpr.constr_expr * Constr.cast_kind option * Constrexpr.constr_expr) -> Constrexpr.constr_expr
val mkLambdaC : (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr) -> Constrexpr.constr_expr
val mkLetInC : (Names.lname * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr) -> Constrexpr.constr_expr
val mkProdC : (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr) -> Constrexpr.constr_expr
val mkAppC : (Constrexpr.constr_expr * Constrexpr.constr_expr list) -> Constrexpr.constr_expr

Basic form of application, collapsing nested applications

val mkLambdaCN : ?⁠loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val mkProdCN : ?⁠loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val mkCLambdaN : ?⁠loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val mkCProdN : ?⁠loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr
Pattern constructors
val mkCPatOr : ?⁠loc:Loc.t -> Constrexpr.cases_pattern_expr list -> Constrexpr.cases_pattern_expr

Interpretation of a list of patterns as a disjunctive pattern (optimized)

val mkAppPattern : ?⁠loc:Loc.t -> Constrexpr.cases_pattern_expr -> Constrexpr.cases_pattern_expr list -> Constrexpr.cases_pattern_expr

Apply a list of pattern arguments to a pattern

Destructors
val coerce_reference_to_id : Libnames.qualid -> Names.Id.t

FIXME: nothing to do here

val coerce_to_id : Constrexpr.constr_expr -> Names.lident

Destruct terms of the form CRef (Ident _).

val coerce_to_name : Constrexpr.constr_expr -> Names.lname

Destruct terms of the form CRef (Ident _) or CHole _.

val coerce_to_cases_pattern_expr : Constrexpr.constr_expr -> Constrexpr.cases_pattern_expr
Binder manipulation
val default_binder_kind : Constrexpr.binder_kind
val names_of_local_binders : Constrexpr.local_binder_expr list -> Names.lname list

Retrieve a list of binding names from a list of binders.

val names_of_local_assums : Constrexpr.local_binder_expr list -> Names.lname list

Same as names_of_local_binder_exprs, but does not take the let bindings into account.

Folds and maps
val fold_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Constrexpr.constr_expr -> 'b) -> 'a -> 'b -> Constrexpr.constr_expr -> 'b

Used in typeclasses

val map_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> Constrexpr.constr_expr -> Constrexpr.constr_expr) -> 'a -> Constrexpr.constr_expr -> Constrexpr.constr_expr
Miscellaneous
val replace_vars_constr_expr : Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val free_vars_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t
val occur_var_constr_expr : Names.Id.t -> Constrexpr.constr_expr -> bool
val names_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t

Return all (non-qualified) names treating binders as names

val ntn_loc : ?⁠loc:Loc.t -> Constrexpr.constr_notation_substitution -> Constrexpr.notation -> (int * int) list
val patntn_loc : ?⁠loc:Loc.t -> Constrexpr.cases_pattern_notation_substitution -> Constrexpr.notation -> (int * int) list
val isCSort : Constrexpr.constr_expr -> bool
val error_invalid_pattern_notation : ?⁠loc:Loc.t -> unit -> 'a

For cases pattern parsing errors