Patterntype 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 constr_pattern = | PRef of Names.GlobRef.t | |
| PVar of Names.Id.t | |
| PEvar of Evar.t * constr_pattern list | |
| 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