package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module NamegenSource

This file features facilities to generate fresh names.

Sourcetype intro_pattern_naming_expr =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous

General evar naming using intro patterns

Sourceval 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
Sourceval id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
Sourceval head_name : Evd.evar_map -> EConstr.types -> Names.Id.t option

Deprecated synonyms of mkProd_name and mkLambda_name

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 : Environ.env -> 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

Sourceval next_name_away_with_default : string -> Names.Name.t -> Names.Id.Set.t -> Names.Id.t
Sourceval 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 =
  1. | RenamingForCasesPattern of Names.Name.t list * EConstr.constr
    (*

    avoid only global constructors

    *)
  2. | RenamingForGoal
    (*

    avoid all globals (as in intro)

    *)
  3. | RenamingElsewhereFor of Names.Name.t list * EConstr.constr
Sourceval make_all_rel_context_name_different : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Environ.env * EConstr.rel_context
Sourceval make_all_name_different : Environ.env -> Evd.evar_map -> Environ.env
Sourceval compute_displayed_name_in_gen : (Evd.evar_map -> int -> 'a -> bool) -> Environ.env -> Evd.evar_map -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct