package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Patterns
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.pretyping/Pattern/index.html

Module Pattern

Patterns
type patvar = Names.Id.t

Cases pattern variables

type case_info_pattern = {
  1. cip_style : Constr.case_style;
  2. cip_ind : Names.inductive option;
  3. cip_extensible : bool;
    (*

    does this match end with _ => _ ?

    *)
}
type 'i uninstantiated_pattern =
  1. | PGenarg : Genarg.glob_generic_argument -> [ `uninstantiated ] uninstantiated_pattern
type 'i constr_pattern_r =
  1. | PRef of Names.GlobRef.t
  2. | PVar of Names.Id.t
  3. | PEvar of Evar.t * 'i constr_pattern_r list
  4. | PRel of int
  5. | PApp of 'i constr_pattern_r * 'i constr_pattern_r array
  6. | PSoApp of patvar * 'i constr_pattern_r list
  7. | PProj of Names.Projection.t * 'i constr_pattern_r
  8. | PLambda of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r
  9. | PProd of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r
  10. | PLetIn of Names.Name.t * 'i constr_pattern_r * 'i constr_pattern_r option * 'i constr_pattern_r
  11. | PSort of UnivGen.QualityOrSet.t
  12. | PMeta of patvar option
  13. | PIf of 'i constr_pattern_r * 'i constr_pattern_r * 'i constr_pattern_r
  14. | 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

    *)
  15. | PFix of int array * int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array
  16. | PCoFix of int * Names.Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array
  17. | PInt of Uint63.t
  18. | PFloat of Float64.t
  19. | PString of Pstring.t
  20. | PArray of 'i constr_pattern_r array * 'i constr_pattern_r * 'i constr_pattern_r
  21. | PUninstantiated of 'i uninstantiated_pattern
type constr_pattern = [ `any ] constr_pattern_r

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

type _ pattern_kind =
  1. | Any
  2. | Uninstantiated : [ `uninstantiated ] pattern_kind