package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

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

Module PatternopsSource

Functions on patterns
Sourceval constr_pattern_eq : Pattern.constr_pattern -> Pattern.constr_pattern -> bool
Sourceval noccurn_pattern : int -> _ Pattern.constr_pattern_r -> bool
Sourceexception BoundPattern

head_pattern_bound t extracts the head variable/constant of the type t or raises BoundPattern (even if a sort); it raises an anomaly if t is an abstraction

Sourceval head_pattern_bound : Pattern.constr_pattern -> Names.GlobRef.t

head_of_constr_reference c assumes r denotes a reference and returns its label; raises an anomaly otherwise

Sourceval head_of_constr_reference : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t
  • deprecated use [EConstr.destRef]

pattern_of_constr c translates a term c with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in c

Sourceval legacy_bad_pattern_of_constr : Environ.env -> Evd.evar_map -> EConstr.constr -> Pattern.constr_pattern

Do not use, for internal Coq use only.

pattern_of_glob_constr l c translates a term c with metavariables into a pattern; variables bound in l are replaced by the pattern to which they are bound

Sourceval uninstantiated_pattern_of_glob_constr : Glob_term.glob_constr -> Names.Id.Set.t * [ `uninstantiated ] Pattern.constr_pattern_r
Sourceval map_pattern_with_binders : (Names.Name.t -> 'a -> 'a) -> ('a -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r) -> 'a -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r
Sourceval lift_pattern : int -> 'i Pattern.constr_pattern_r -> 'i Pattern.constr_pattern_r

Interp genargs

Sourceval interp_pattern : [ `uninstantiated ] Pattern.constr_pattern_r pat_interp_fun
Sourceval register_interp_pat : (_, 'g, _) Genarg.genarg_type -> 'g pat_interp_fun -> unit