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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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