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 option * 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