Equations
- Lean.binductionOnSuffix = "binductionOn"
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
@[export lean_is_aux_recursor]
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Instances For
@[export lean_is_no_confusion]