Module Pattern

Patterns
type patvar = Names.Id.t

Cases pattern variables

type case_info_pattern = {
cip_style : Constr.case_style;
cip_ind : Names.inductive option;
cip_ind_tags : bool list option;

indicates LetIn/Lambda in arity

cip_extensible : bool;

does this match end with _ => _ ?

}
type constr_pattern =
| PRef of Names.GlobRef.t
| PVar of Names.Id.t
| PEvar of Evar.t * constr_pattern array
| 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 * constr_pattern * constr_pattern * (int * bool list * 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