def Lean.Elab.Deriving.FromToJson.mkToJsonHeader (indVal : InductiveVal) : TermElabM Header

Equations

• Lean.Elab.Deriving.FromToJson.mkToJsonHeader indVal = Lean.Elab.Deriving.mkHeader `Lean.ToJson 1 indVal

def Lean.Elab.Deriving.FromToJson.mkFromJsonHeader (indVal : InductiveVal) : TermElabM Header

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkJsonField (n : Name) : CoreM (Bool × Term)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Deriving.FromToJson.mkJsonField n = Lean.throwError (Lean.toMessageData "invalid json field name " ++ Lean.toMessageData n ++ Lean.toMessageData "")

def Lean.Elab.Deriving.FromToJson.mkToJsonBodyForStruct (header : Header) (indName : Name) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonBodyForInduct (ctx : Context) (header : Header) (indName : Name) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonBodyForInduct.mkAlts (indVal : InductiveVal) (rhs : ConstructorVal → Array (Ident × Expr) → Option (Array Name) → TermElabM Term) : TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonBodyForStruct (indName : Name) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonBodyForInduct (ctx : Context) (indName : Name) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonBodyForInduct.mkAlts (ctx : Context) (indVal : InductiveVal) : TermElabM (Array Term)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonBody (ctx : Context) (header : Header) (e : Expr) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonBody (ctx : Context) (e : Expr) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonMutualBlock (ctx : Context) : TermElabM Command

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonMutualBlock (ctx : Context) : TermElabM Command

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler (declNames : Array Name) : Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler (declNames : Array Name) : Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.