- motive : RecursorUnivLevelPos
- majorType (idx : Nat) : RecursorUnivLevelPos
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.