source
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

Instances For

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

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

Instances For

source
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)

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For