package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.pretyping/Unification/index.html
Module UnificationSource
Meta machinery
These functions are almost deprecated. They were used before the introduction of the full-fledged evar calculus. In an ideal world, they should be removed. Alas, some parts of the code still use them. Do not use in newly-written code.
module Metaset : Util.Set.S with type elt = Constr.metavariablemodule Metamap :
Util.Map.ExtS with type key = Constr.metavariable and module Set := MetasetLegacy unification
Source
type core_unify_flags = {modulo_conv_on_closed_terms : TransparentState.t option;use_metas_eagerly_in_conv_on_closed_terms : bool;use_evars_eagerly_in_conv_on_closed_terms : bool;modulo_delta : TransparentState.t;modulo_delta_types : TransparentState.t;check_applied_meta_types : bool;use_pattern_unification : bool;use_meta_bound_pattern_unification : bool;allowed_evars : Evarsolve.AllowedEvars.t;restrict_conv_on_strict_subterms : bool;modulo_betaiota : bool;modulo_eta : bool;
}Source
type unify_flags = {core_unify_flags : core_unify_flags;merge_unify_flags : core_unify_flags;subterm_unify_flags : core_unify_flags;allow_K_in_toplevel_higher_order_unification : bool;resolve_evars : bool;
}Source
val w_unify :
?metas:Meta.t ->
Environ.env ->
Evd.evar_map ->
Evd.conv_pb ->
?flags:unify_flags ->
EConstr.constr ->
EConstr.constr ->
Meta.t * Evd.evar_mapThe "unique" unification function
Source
val w_unify_to_subterm :
?metas:Meta.t ->
Environ.env ->
Evd.evar_map ->
?flags:unify_flags ->
(EConstr.constr * EConstr.constr) ->
(Meta.t * Evd.evar_map) * EConstr.constrw_unify_to_subterm env m (c,t) performs unification of c with a subterm of t. Constraints are added to m and the matched subterm of t is also returned.
Source
val w_unify_to_subterm_all :
?metas:Meta.t ->
Environ.env ->
Evd.evar_map ->
?flags:unify_flags ->
(EConstr.constr * EConstr.constr) ->
(Meta.t * Evd.evar_map) listSource
val w_unify_meta_types :
?metas:Meta.t ->
Environ.env ->
?flags:unify_flags ->
Evd.evar_map ->
Meta.t * Evd.evar_mapSource
val w_coerce_to_type :
?metas:Meta.t ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types ->
EConstr.types ->
Evd.evar_map * Meta.t * EConstr.constrw_coerce_to_type env evd c ctyp typ tries to coerce c of type ctyp so that its gets type typ; typ may contain metavariables
Source
type abstraction_request = | AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map option * EConstr.constr * Locus.clause| AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool
Source
type 'r abstraction_result =
Names.Id.t
* Environ.named_context_val
* EConstr.named_declaration list
* Names.Id.t option
* EConstr.types
* (Evd.evar_map * EConstr.constr) optionSource
val make_abstraction :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
abstraction_request ->
'r abstraction_resultSource
val pose_all_metas_as_evars :
metas:Meta.t ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Evd.evar_map * Meta.t * EConstr.constrSource
val abstract_list_all :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.constr ->
EConstr.constr list ->
Evd.evar_map * (EConstr.constr * EConstr.types)abstract_list_all env evd t c l abstracts the terms in l over c to get a term of type t (exported for inv.ml)
On This Page