Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
def
Lean.Elab.Deriving.FromToJson.mkToJsonBodyForInduct.mkAlts
(indVal : InductiveVal)
(rhs : ConstructorVal → Array (Ident × Expr) → Option (Array Name) → TermElabM Term)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Deriving.FromToJson.mkFromJsonBodyForInduct.mkAlts
(ctx : Context)
(indVal : InductiveVal)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.