Module `Namegen`Source

This file features facilities to generate fresh names.

Sourcetype intro_pattern_naming_expr =

| IntroIdentifier of Names.Id.t
| IntroFresh of Names.Id.t
| IntroAnonymous

General evar naming using intro patterns

val intro_pattern_naming_eq : 
  intro_pattern_naming_expr ->
  intro_pattern_naming_expr ->
  bool

Equalities on intro_pattern_naming

Sourceval default_prop_ident : Names.Id.t

Sourceval default_small_ident : Names.Id.t

Sourceval default_type_ident : Names.Id.t

Sourceval default_non_dependent_ident : Names.Id.t

Sourceval default_dependent_ident : Names.Id.t

Sourceval lowercase_first_char : Names.Id.t -> string

Sourceval sort_hdchar : Sorts.t -> string

Sourceval hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string

Source

val id_of_name_using_hdchar : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Names.Name.t ->
  Names.Id.t

Source

val named_hd : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Names.Name.t ->
  Names.Name.t

Sourceval head_name : Evd.evar_map -> EConstr.types -> Names.Id.t option

Source

val mkProd_name : 
  Environ.env ->
  Evd.evar_map ->
  (Names.Name.t Context.binder_annot * EConstr.types * EConstr.types) ->
  EConstr.types

Source

val mkLambda_name : 
  Environ.env ->
  Evd.evar_map ->
  (Names.Name.t Context.binder_annot * EConstr.types * EConstr.constr) ->
  EConstr.constr

Source

val prod_name : 
  Environ.env ->
  Evd.evar_map ->
  (Names.Name.t Context.binder_annot * EConstr.types * EConstr.types) ->
  EConstr.types

Deprecated synonyms of mkProd_name and mkLambda_name

Source

val lambda_name : 
  Environ.env ->
  Evd.evar_map ->
  (Names.Name.t Context.binder_annot * EConstr.types * EConstr.constr) ->
  EConstr.constr

Source

val prod_create : 
  Environ.env ->
  Evd.evar_map ->
  (Sorts.relevance * EConstr.types * EConstr.types) ->
  EConstr.constr

Source

val lambda_create : 
  Environ.env ->
  Evd.evar_map ->
  (Sorts.relevance * EConstr.types * EConstr.constr) ->
  EConstr.constr

Source

val name_assumption : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_declaration ->
  EConstr.rel_declaration

Source

val name_context : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  EConstr.rel_context

Source

val mkProd_or_LetIn_name : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.rel_declaration ->
  EConstr.types

Source

val mkLambda_or_LetIn_name : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.rel_declaration ->
  EConstr.constr

Source

val it_mkProd_or_LetIn_name : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.rel_context ->
  EConstr.types

Source

val it_mkLambda_or_LetIn_name : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.rel_context ->
  EConstr.constr

Sourceval next_ident_away_from : Names.Id.t -> (Names.Id.t -> bool) -> Names.Id.t

Avoid clashing with a name satisfying some predicate

Sourceval next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

next_ident_away original_id unwanted_ids returns a new identifier as close as possible to the original_id while avoiding all unwanted_ids.

In particular:

if original_id does not appear in the list of unwanted_ids, then original_id is returned.
if original_id appears in the list of unwanted_ids, then this function returns a new id that:
- has the same root as the original_id,
- does not occur in the list of unwanted_ids,
- has the smallest possible subscript.

where by subscript of some identifier we mean last part of it that is composed only from (decimal) digits and by root of some identifier we mean the whole identifier except for the subscript.

E.g. if we take foo42, then 42 is the subscript, and foo is the root.

Sourceval next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module

Sourceval next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals

Sourceval next_name_away : Names.Name.t -> Names.Id.Set.t -> Names.Id.t

Default is default_non_dependent_ident

Source

val next_name_away_with_default : 
  string ->
  Names.Name.t ->
  Names.Id.Set.t ->
  Names.Id.t

Source

val next_name_away_with_default_using_types : 
  string ->
  Names.Name.t ->
  Names.Id.Set.t ->
  EConstr.types ->
  Names.Id.t

Sourceval set_reserved_typed_name : (EConstr.types -> Names.Name.t) -> unit

Sourcetype renaming_flags =

| RenamingForCasesPattern of Names.Name.t list * EConstr.constr
(*
avoid only global constructors
*)
| RenamingForGoal
(*
avoid all globals (as in intro)
*)
| RenamingElsewhereFor of Names.Name.t list * EConstr.constr

Sourceval make_all_name_different : Environ.env -> Evd.evar_map -> Environ.env

Source

val compute_displayed_name_in : 
  Evd.evar_map ->
  renaming_flags ->
  Names.Id.Set.t ->
  Names.Name.t ->
  EConstr.constr ->
  Names.Name.t * Names.Id.Set.t

Source

val compute_and_force_displayed_name_in : 
  Evd.evar_map ->
  renaming_flags ->
  Names.Id.Set.t ->
  Names.Name.t ->
  EConstr.constr ->
  Names.Name.t * Names.Id.Set.t

Source

val compute_displayed_let_name_in : 
  Evd.evar_map ->
  renaming_flags ->
  Names.Id.Set.t ->
  Names.Name.t ->
  'a ->
  Names.Name.t * Names.Id.Set.t

Source

val rename_bound_vars_as_displayed : 
  Evd.evar_map ->
  Names.Id.Set.t ->
  Names.Name.t list ->
  EConstr.types ->
  EConstr.types

Source

val compute_displayed_name_in_gen : 
  (Evd.evar_map -> int -> 'a -> bool) ->
  Evd.evar_map ->
  Names.Id.Set.t ->
  Names.Name.t ->
  'a ->
  Names.Name.t * Names.Id.Set.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.engine/Namegen/index.html

Module `Namegen`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.engine/Namegen/index.html

Module NamegenSource

Module `Namegen`Source