Constrexpr_opsConstrexpr_ops: utilities on constr_expr
constr_expr related typesval sort_name_expr_eq : Constrexpr.sort_name_expr -> Constrexpr.sort_name_expr -> boolval univ_level_expr_eq : Constrexpr.univ_level_expr -> Constrexpr.univ_level_expr -> boolval sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> boolval explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> boolEquality on explicitation.
val constr_expr_eq_gen : (Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool) -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> boolval constr_expr_eq : Constrexpr.constr_expr -> Constrexpr.constr_expr -> boolEquality 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 -> boolEquality on local_binder_expr. Same properties as constr_expr_eq.
val binder_kind_eq : Constrexpr.binder_kind -> Constrexpr.binder_kind -> boolEquality on binder_kind
val constr_loc : Constrexpr.constr_expr -> Loc.t optionval cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t optionval local_binders_loc : Constrexpr.local_binder_expr list -> Loc.t optionBasic form of the corresponding constructors
val mkIdentC : Names.Id.t -> Constrexpr.constr_exprval mkRefC : Libnames.qualid -> Constrexpr.constr_exprval mkCastC : (Constrexpr.constr_expr * Constr.cast_kind * Constrexpr.constr_expr) -> Constrexpr.constr_exprval mkLambdaC : (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr) -> Constrexpr.constr_exprval mkLetInC : (Names.lname * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr) -> Constrexpr.constr_exprval mkProdC : (Names.lname list * Constrexpr.binder_kind * Constrexpr.constr_expr * Constrexpr.constr_expr) -> Constrexpr.constr_exprval mkAppC : (Constrexpr.constr_expr * Constrexpr.constr_expr list) -> Constrexpr.constr_exprBasic form of application, collapsing nested applications
Optimized constructors: does not add a constructor for an empty binder list
val mkLambdaCN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_exprval mkProdCN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_exprAliases for the corresponding constructors; generally mkLambdaCN and mkProdCN should be preferred
val mkCLambdaN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_exprval mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_exprval mkCPatOr : ?loc:Loc.t -> Constrexpr.cases_pattern_expr list -> Constrexpr.cases_pattern_exprInterpretation 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_exprApply a list of pattern arguments to a pattern
val coerce_reference_to_id : Libnames.qualid -> Names.Id.tFIXME: nothing to do here
val coerce_to_id : Constrexpr.constr_expr -> Names.lidentDestruct terms of the form CRef (Ident _).
val coerce_to_name : Constrexpr.constr_expr -> Names.lnameDestruct terms of the form CRef (Ident _) or CHole _.
val coerce_to_cases_pattern_expr : Constrexpr.constr_expr -> Constrexpr.cases_pattern_exprval default_binder_kind : Constrexpr.binder_kindval names_of_local_binders : Constrexpr.local_binder_expr list -> Names.lname listRetrieve a list of binding names from a list of binders.
val names_of_local_assums : Constrexpr.local_binder_expr list -> Names.lname listSame as names_of_local_binder_exprs, but does not take the let bindings into account.
val fold_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Constrexpr.constr_expr -> 'b) -> 'a -> 'b -> Constrexpr.constr_expr -> 'bUsed in typeclasses
Used in correctness and interface; absence of var capture not guaranteed in pattern-matching clauses and in binders of the form x,y:T(x)
val map_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> Constrexpr.constr_expr -> Constrexpr.constr_expr) -> 'a -> Constrexpr.constr_expr -> Constrexpr.constr_exprval replace_vars_constr_expr : Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_exprval free_vars_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.tval occur_var_constr_expr : Names.Id.t -> Constrexpr.constr_expr -> boolval names_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.tReturn all (non-qualified) names treating binders as names
val split_at_annot : Constrexpr.local_binder_expr list -> Names.lident option -> Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr listval ntn_loc : ?loc:Loc.t -> Constrexpr.constr_notation_substitution -> Constrexpr.notation -> (int * int) listval patntn_loc : ?loc:Loc.t -> Constrexpr.cases_pattern_notation_substitution -> Constrexpr.notation -> (int * int) listval error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'aFor cases pattern parsing errors