package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Coercions.
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.pretyping/Coercion/index.html

Module CoercionSource

Coercions.
Sourcetype coercion_trace
Sourceval empty_coercion_trace : coercion_trace
Sourceval reapply_coercions : Evd.evar_map -> coercion_trace -> EConstr.t -> EConstr.t
Sourceval inh_coerce_to_sort : ?loc:Loc.t -> ?use_coercions:bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_type_judgment

inh_coerce_to_sort env isevars j coerces j to a type; i.e. it inserts a coercion into j, if needed, in such a way it gets as type a sort; it fails if no coercion is applicable

Sourceval inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_judgment

inh_coerce_to_base env isevars j coerces j to its base type; i.e. it inserts a coercion into j, if needed, in such a way it gets as type its base type (the notion depends on the coercion system)

remove_subset env sigma t applies program mode transformations to t, recursively transforming {x : A | P} into A

inh_conv_coerce_to resolve_tc Loc.t env isevars j t coerces j to an object of type t; i.e. it inserts a coercion into j, if needed, in such a way t and j.uj_type are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing)

Sourceval inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool -> ?patvars_abstract:bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option
Sourceval inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool -> ?patvars_abstract:bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option

inh_pattern_coerce_to loc env isevars pat ind1 ind2 coerces the Cases pattern pat typed in ind1 into a pattern typed in ind2; raises Not_found if no coercion found

Sourcetype expected =
  1. | Type of EConstr.types
  2. | Sort
  3. | Product
Sourceval register_hook : name:string -> ?override:bool -> hook -> unit

A plugin can override the coercion mechanism by registering a hook here. Note that these hooks will only be trigerred when no direct or reversible coercion applies. Newly registered hooks are not active by default, see activate_hook below. The same hook cannot be registered twice, except if override is true. Beware that this addition is not persistent, it is up to the plugin to use libobject if needed.

Sourceval activate_hook : name:string -> unit

Activate a previously registered hook. Most recently activated hooks are tried first.

Sourceval deactivate_hook : name:string -> unit

Deactivate a hook. If the hook wasn't registered/active, this does nothing.

Sourcetype delayed_app_body
Sourceval start_app_body : Evd.evar_map -> EConstr.constr -> delayed_app_body
Sourceval force_app_body : delayed_app_body -> EConstr.constr
Sourceval reapply_coercions_body : Evd.evar_map -> coercion_trace -> delayed_app_body -> delayed_app_body
Sourceval inh_app_fun : program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> delayed_app_body -> EConstr.types -> Evd.evar_map * delayed_app_body * EConstr.types * coercion_trace

inh_app_fun resolve_tc env isevars j coerces j to a function; i.e. it inserts a coercion into j, if needed, in such a way it gets as type a product; it returns j if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing)