package coq

  1. Overview
  2. Docs
On This Page
  1. Patterns
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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

Module PatternSource

Patterns
Sourcetype patvar = Names.Id.t

Cases pattern variables

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

    does this match end with _ => _ ?

    *)
}
Sourcetype constr_pattern =
  1. | PRef of Names.GlobRef.t
  2. | PVar of Names.Id.t
  3. | PEvar of constr_pattern Constr.pexistential
  4. | PRel of int
  5. | PApp of constr_pattern * constr_pattern array
  6. | PSoApp of patvar * constr_pattern list
  7. | PProj of Names.Projection.t * constr_pattern
  8. | PLambda of Names.Name.t * constr_pattern * constr_pattern
  9. | PProd of Names.Name.t * constr_pattern * constr_pattern
  10. | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
  11. | PSort of Sorts.family
  12. | PMeta of patvar option
  13. | PIf of constr_pattern * constr_pattern * constr_pattern
  14. | 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

    *)
  15. | PFix of int array * int * Names.Name.t array * constr_pattern array * constr_pattern array
  16. | PCoFix of int * Names.Name.t array * constr_pattern array * constr_pattern array
  17. | PInt of Uint63.t
  18. | PFloat of Float64.t
  19. | 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