package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz

sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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

Module `Pattern`Source

Patterns

Sourcetype patvar = Names.Id.t

Cases pattern variables

Sourcetype case_info_pattern = {

cip_style : Constr.case_style;
cip_ind : Names.inductive option;
cip_extensible : bool;
(*
does this match end with _ => _ ?
*)

}

Sourcetype constr_pattern =

| PRef of Names.GlobRef.t
| PVar of Names.Id.t
| PEvar of Evar.t * constr_pattern list
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
| PProj of Names.Projection.t * constr_pattern
| PLambda of Names.Name.t * constr_pattern * constr_pattern
| PProd of Names.Name.t * constr_pattern * constr_pattern
| PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
| PSort of Sorts.family
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * (Names.Name.t array * constr_pattern) option * constr_pattern * (int * Names.Name.t array * constr_pattern) list
(*
index of constructor, nb of args
*)
| PFix of int array * int * Names.Name.t array * constr_pattern array * constr_pattern array
| PCoFix of int * Names.Name.t array * constr_pattern array * constr_pattern array
| PInt of Uint63.t
| PFloat of Float64.t
| PArray of constr_pattern array * constr_pattern * constr_pattern

Nota : in a PCase, the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch

On This Page

Patterns