Documentation

Lean.Elab.Deriving.FromToJson

def Lean.Elab.Deriving.FromToJson.mkJsonField (n : Lean.Name) :

Bool × Lean.Term

Equations

Lean.Elab.Deriving.FromToJson.mkJsonField n = let s := Lean.Name.toString n; let s₁ := String.dropRightWhile s fun a => a == Char.ofNat 63; (s != s₁, { raw := (Lean.Syntax.mkStrLit s₁).raw })

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

Lean.Elab.Command.CommandElabM Bool

Equations

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

def Lean.Elab.Deriving.FromToJson.mkToJsonInstanceHandler.mkAlts (indVal : Lean.InductiveVal) (rhs : Lean.ConstructorVal → Array (Lean.Ident × Lean.Expr) → Option (Array Lean.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.

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

Lean.Elab.Command.CommandElabM Bool

Equations

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

def Lean.Elab.Deriving.FromToJson.mkFromJsonInstanceHandler.mkAlts (indVal : Lean.InductiveVal) (fromJsonFuncId : Lean.Ident) :

Lean.Elab.TermElabM (Array Lean.Term)

Equations

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