- recArgPos : Nat
- fixedParamPerms : FixedParamPerms
Instances For
def
Lean.Elab.Structural.registerEqnsInfo
(preDef : PreDefinition)
(declNames : Array Name)
(recArgPos : Nat)
(fixedParamPerms : FixedParamPerms)
:
Equations
- One or more equations did not get rendered due to their size.