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.mkToJsonInstance.mkAlts
(indVal : Lean.InductiveVal)
(rhs : Lean.ConstructorVal → Array (Lean.Ident × Lean.Expr) → Option (Array Lake.Name) → Lean.Elab.TermElabM Lean.Term)
:
Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))
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.mkFromJsonInstance.mkAlts
(indVal : Lean.InductiveVal)
(fromJsonFuncId : Lean.Ident)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler declNames = Array.foldlM (fun (b : Bool) (n : Lake.Name) => pure b <&&> Lean.Elab.Deriving.FromToJson.mkToJsonInstance n) true declNames 0
Instances For
Equations
- One or more equations did not get rendered due to their size.