package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
doc/coq-core.pretyping/Pattern/index.html
Module Pattern
Patterns
type patvar = Names.Id.tCases pattern variables
type case_info_pattern = {cip_style : Constr.case_style;cip_ind : Names.inductive option;cip_extensible : bool;(*does this match end with _ => _ ?
*)
}type 'i uninstantiated_pattern = | PGenarg : Genarg.glob_generic_argument -> [ `uninstantiated ] uninstantiated_pattern
type 'i constr_pattern_r = | PRef of Names.GlobRef.t| PVar of Names.Id.t| PEvar of Evar.t * 'i constr_pattern_r list| PRel of int| PApp of 'i constr_pattern_r * 'i constr_pattern_r array| PSoApp of patvar * 'i constr_pattern_r list| PProj of Names.Projection.t * 'i constr_pattern_r| PLambda of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r| PProd of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r| PLetIn of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r option * 'i constr_pattern_r| PSort of Sorts.family| PMeta of patvar option| PIf of 'i constr_pattern_r * 'i constr_pattern_r * 'i constr_pattern_r| PCase of case_info_pattern * (Names.Name.t array * 'i constr_pattern_r) option * 'i constr_pattern_r * (int * Names.Name.t array * 'i constr_pattern_r) list(*index of constructor, nb of args
*)| PFix of int array * int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array| PCoFix of int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array| PInt of Uint63.t| PFloat of Float64.t| PArray of 'i constr_pattern_r array * 'i constr_pattern_r * 'i constr_pattern_r| PUninstantiated of 'i uninstantiated_pattern
type constr_pattern = [ `any ] constr_pattern_rNota : in a PCase, the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch
On This Page