package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.pretyping/Evarsolve/index.html

Module EvarsolveSource

Sourcetype alias
Sourceval of_alias : alias -> EConstr.t
Sourcemodule AllowedEvars : sig ... end
Sourcetype unify_flags = {
  1. modulo_betaiota : bool;
  2. open_ts : TransparentState.t;
  3. closed_ts : TransparentState.t;
  4. subterm_ts : TransparentState.t;
  5. allowed_evars : AllowedEvars.t;
  6. allow_K_at_toplevel : bool;
  7. with_cs : bool;
}
Sourcetype unification_result =
  1. | Success of Evd.evar_map
  2. | UnifFailure of Evd.evar_map * Pretype_errors.unification_error
Sourceval is_success : unification_result -> bool
Sourceval is_evar_allowed : unify_flags -> Evar.t -> bool
Sourceval expand_vars_in_term : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr

Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context

One might want to use different conversion strategies for types and terms: e.g. preventing delta reductions when doing term unifications but allowing arbitrary delta conversion when checking the types of evar instances.

Sourcetype unification_kind =
  1. | TypeUnification
  2. | TermUnification

A unification function parameterized by:

  • unification flags
  • the kind of unification
  • environment
  • sigma
  • conversion problem
  • the two terms to unify.

A conversion function: parameterized by the kind of unification, environment, sigma, conversion problem and the two terms to convert. Conversion is not allowed to instantiate evars contrary to unification.

instantiate_evar unify flags env sigma ev c defines the evar ev with c, checking that the type of c is unifiable with ev's declared type first.

Preconditions:

  • ev does not occur in c.
  • c does not contain any Meta(_)

If ev and c have non inferably convertible types, an exception IllTypedInstance is raised

evar_define choose env ev c try to instantiate ev with c (typed in env), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given ev; If ev and c have non inferably convertible types, an exception IllTypedInstance is raised

Sourceval evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map
Sourceval refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool -> ?refreshset:bool -> bool option -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
Sourceval solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> Evar.t -> EConstr.constr list -> EConstr.constr list -> Evd.evar_map
Sourceval solve_evar_evar : ?force:bool -> (Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map) -> unifier -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.existential -> Evd.evar_map

The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised

Sourceval solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> (bool option * EConstr.existential * EConstr.constr) -> unification_result
Sourceval reconsider_unif_constraints : unifier -> unify_flags -> Evd.evar_map -> unification_result
Sourceval is_unification_pattern_evar : Environ.env -> Evd.evar_map -> EConstr.existential -> EConstr.constr list -> EConstr.constr -> alias list option
Sourceval is_unification_pattern : (Environ.env * int) -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr -> alias list option
Sourceval solve_pattern_eqn : Environ.env -> Evd.evar_map -> alias list -> EConstr.constr -> EConstr.constr
Sourceval noccur_evar : Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> bool
Sourceexception IllTypedInstance of Environ.env * Evd.evar_map * EConstr.types * EConstr.types

May raise IllTypedInstance if types are not convertible

Sourceval remove_instance_local_defs : Evd.evar_map -> Evar.t -> 'a list -> 'a list
Sourceval get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types