package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

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

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.1.tar.gz

sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

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 constr_pattern Constr.pexistential
| 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