Module `Constrexpr_ops`Source

Constrexpr_ops: utilities on constr_expr

Equalities on `constr_expr` related types

val sort_name_expr_eq : 
  Constrexpr.sort_name_expr ->
  Constrexpr.sort_name_expr ->
  bool

Source

val univ_level_expr_eq : 
  Constrexpr.univ_level_expr ->
  Constrexpr.univ_level_expr ->
  bool

Sourceval sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> bool

Source

val explicitation_eq : 
  Constrexpr.explicitation ->
  Constrexpr.explicitation ->
  bool

Equality on explicitation.

Source

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

Sourceval 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.

Source

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

Equality on local_binder_expr. Same properties as constr_expr_eq.

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

Equality on binder_kind

Retrieving locations

Sourceval constr_loc : Constrexpr.constr_expr -> Loc.t option

Sourceval cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t option

Sourceval local_binders_loc : Constrexpr.local_binder_expr list -> Loc.t option

Constructors

Term constructors

Basic form of the corresponding constructors

Sourceval mkIdentC : Names.Id.t -> Constrexpr.constr_expr

Sourceval mkRefC : Libnames.qualid -> Constrexpr.constr_expr

Source

val mkCastC : 
  (Constrexpr.constr_expr * Constr.cast_kind * Constrexpr.constr_expr) ->
  Constrexpr.constr_expr

Source

val mkLambdaC : 
  (Names.lname list
   * Constrexpr.binder_kind
   * Constrexpr.constr_expr
   * Constrexpr.constr_expr) ->
  Constrexpr.constr_expr

Source

val mkLetInC : 
  (Names.lname
   * Constrexpr.constr_expr
   * Constrexpr.constr_expr option
   * Constrexpr.constr_expr) ->
  Constrexpr.constr_expr

Source

val mkProdC : 
  (Names.lname list
   * Constrexpr.binder_kind
   * Constrexpr.constr_expr
   * Constrexpr.constr_expr) ->
  Constrexpr.constr_expr

Source

val mkAppC : 
  (Constrexpr.constr_expr * Constrexpr.constr_expr list) ->
  Constrexpr.constr_expr

Basic form of application, collapsing nested applications

Optimized constructors: does not add a constructor for an empty binder list

Source

val mkLambdaCN : 
  ?loc:Loc.t ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Source

val mkProdCN : 
  ?loc:Loc.t ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Aliases for the corresponding constructors; generally mkLambdaCN and mkProdCN should be preferred

Source

val mkCLambdaN : 
  ?loc:Loc.t ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Source

val mkCProdN : 
  ?loc:Loc.t ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Pattern constructors

Source

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)

Source

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

Sourceval coerce_reference_to_id : Libnames.qualid -> Names.Id.t

FIXME: nothing to do here

Sourceval coerce_to_id : Constrexpr.constr_expr -> Names.lident

Destruct terms of the form CRef (Ident _).

Sourceval coerce_to_name : Constrexpr.constr_expr -> Names.lname

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

Source

val coerce_to_cases_pattern_expr : 
  Constrexpr.constr_expr ->
  Constrexpr.cases_pattern_expr

Binder manipulation

Sourceval default_binder_kind : Constrexpr.binder_kind

Source

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

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

Source

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

Source

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

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)

Source

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

Source

val replace_vars_constr_expr : 
  Names.Id.t Names.Id.Map.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Sourceval free_vars_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t

Sourceval occur_var_constr_expr : Names.Id.t -> Constrexpr.constr_expr -> bool

Sourceval names_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t

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

Source

val split_at_annot : 
  Constrexpr.local_binder_expr list ->
  Names.lident option ->
  Constrexpr.local_binder_expr list * Constrexpr.local_binder_expr list

Source

val ntn_loc : 
  ?loc:Loc.t ->
  Constrexpr.constr_notation_substitution ->
  Constrexpr.notation ->
  (int * int) list

Source

val patntn_loc : 
  ?loc:Loc.t ->
  Constrexpr.cases_pattern_notation_substitution ->
  Constrexpr.notation ->
  (int * int) list

Sourceval error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a

For cases pattern parsing errors

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Constrexpr_ops/index.html

Module `Constrexpr_ops`Source

Retrieving locations

Constructors

Term constructors

Pattern constructors

Destructors

Binder manipulation

Folds and maps

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Constrexpr_ops/index.html

Module Constrexpr_opsSource

Equalities on constr_expr related types

Retrieving locations

Constructors

Term constructors

Pattern constructors

Destructors

Binder manipulation

Folds and maps

Module `Constrexpr_ops`Source

Equalities on `constr_expr` related types