package coq-core

  1. Overview
  2. Docs
On This Page
  1. Coercions.
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Coercions.
type coercion_trace
val empty_coercion_trace : coercion_trace
val reapply_coercions : Evd.evar_map -> coercion_trace -> EConstr.t -> EConstr.t
val 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

val 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)

val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option
val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:bool -> ?use_coercions: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

type delayed_app_body
val start_app_body : Evd.evar_map -> EConstr.constr -> delayed_app_body
val force_app_body : delayed_app_body -> EConstr.constr
val reapply_coercions_body : Evd.evar_map -> coercion_trace -> delayed_app_body -> delayed_app_body
val inh_app_fun : program_mode:bool -> resolve_tc:bool -> ?use_coercions:bool -> Environ.env -> Evd.evar_map -> 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)

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