class Lean.FromJson (α : Type u) : Type u

• fromJson? : Lean.Json → Except String α

class Lean.ToJson (α : Type u) : Type u

• toJson : α → Lean.Json

instance Lean.instFromJsonJson : Lean.FromJson Lean.Json

instance Lean.instToJsonJson : Lean.ToJson Lean.Json

Equations

• Lean.instToJsonJson = { toJson := id }

instance Lean.instFromJsonJsonNumber : Lean.FromJson Lean.JsonNumber

Equations

• Lean.instFromJsonJsonNumber = { fromJson? := Lean.Json.getNum? }

instance Lean.instToJsonJsonNumber : Lean.ToJson Lean.JsonNumber

Equations

• Lean.instToJsonJsonNumber = { toJson := Lean.Json.num }

instance Lean.instFromJsonEmpty : Lean.FromJson Empty

Equations

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

instance Lean.instToJsonEmpty : Lean.ToJson Empty

instance Lean.instFromJsonBool : Lean.FromJson Bool

instance Lean.instToJsonBool : Lean.ToJson Bool

Equations

• Lean.instToJsonBool = { toJson := fun (b : Bool) => Lean.Json.bool b }

instance Lean.instFromJsonNat : Lean.FromJson Nat

Equations

• Lean.instFromJsonNat = { fromJson? := Lean.Json.getNat? }

instance Lean.instToJsonNat : Lean.ToJson Nat

instance Lean.instFromJsonInt : Lean.FromJson Int

instance Lean.instToJsonInt : Lean.ToJson Int

instance Lean.instFromJsonString : Lean.FromJson String

instance Lean.instToJsonString : Lean.ToJson String

Equations

• Lean.instToJsonString = { toJson := fun (s : String) => Lean.Json.str s }

instance Lean.instFromJsonFilePath : Lean.FromJson System.FilePath

Equations

• Lean.instFromJsonFilePath = { fromJson? := fun (j : Lean.Json) => System.FilePath.mk <$> j.getStr? }

instance Lean.instToJsonFilePath : Lean.ToJson System.FilePath

instance Lean.instFromJsonArray {α : Type u_1} [Lean.FromJson α] : Lean.FromJson (Array α)

Equations

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

instance Lean.instToJsonArray {α : Type u_1} [Lean.ToJson α] : Lean.ToJson (Array α)

Equations

• Lean.instToJsonArray = { toJson := fun (a : Array α) => Lean.Json.arr (Array.map Lean.toJson a) }

instance Lean.instFromJsonList {α : Type u_1} [Lean.FromJson α] : Lean.FromJson (List α)

Equations

• Lean.instFromJsonList = { fromJson? := fun (j : Lean.Json) => Except.map Array.toList (Lean.fromJson? j) }

instance Lean.instToJsonList {α : Type u_1} [Lean.ToJson α] : Lean.ToJson (List α)

instance Lean.instFromJsonOption {α : Type u_1} [Lean.FromJson α] : Lean.FromJson (Option α)

Equations

• Lean.instFromJsonOption = { fromJson? := fun (x : Lean.Json) => match x with | Lean.Json.null => Except.ok none | j => some <$> Lean.fromJson? j }

instance Lean.instToJsonOption {α : Type u_1} [Lean.ToJson α] : Lean.ToJson (Option α)

Equations

• Lean.instToJsonOption = { toJson := fun (x : Option α) => match x with | none => Lean.Json.null | some a => Lean.toJson a }

instance Lean.instFromJsonProd {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] : Lean.FromJson (α × β)

Equations

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

instance Lean.instToJsonProd {α : Type u_1} {β : Type u_2} [Lean.ToJson α] [Lean.ToJson β] : Lean.ToJson (α × β)

instance Lean.instFromJsonName : Lean.FromJson Lean.Name

instance Lean.instToJsonName : Lean.ToJson Lean.Name

def Lean.bignumFromJson? (j : Lean.Json) : Except String Nat

Note that USizes and UInt64s are stored as strings because JavaScript cannot represent 64-bit numbers.

Equations

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

def Lean.bignumToJson (n : Nat) : Lean.Json

instance Lean.instFromJsonUSize : Lean.FromJson USize

Equations

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

instance Lean.instToJsonUSize : Lean.ToJson USize

instance Lean.instFromJsonUInt64 : Lean.FromJson UInt64

instance Lean.instToJsonUInt64 : Lean.ToJson UInt64

instance Lean.instToJsonFloat : Lean.ToJson Float

Equations

• Lean.instToJsonFloat = { toJson := fun (x : Float) => match Lean.JsonNumber.fromFloat? x with | Sum.inl e => Lean.Json.str e | Sum.inr n => Lean.Json.num n }

instance Lean.instFromJsonFloat : Lean.FromJson Float

instance Lean.instToJsonRBMapString {α : Type} {cmp : String → String → Ordering} [Lean.ToJson α] : Lean.ToJson (Lean.RBMap String α cmp)

instance Lean.instFromJsonRBMapString {α : Type} {cmp : String → String → Ordering} [Lean.FromJson α] : Lean.FromJson (Lean.RBMap String α cmp)

Equations

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

instance Lean.Json.instFromJsonStructured : Lean.FromJson Lean.Json.Structured

instance Lean.Json.instToJsonStructured : Lean.ToJson Lean.Json.Structured

def Lean.Json.toStructured? {α : Type u_1} [Lean.ToJson α] (v : α) : Except String Lean.Json.Structured

def Lean.Json.getObjValAs? (j : Lean.Json) (α : Type u) [Lean.FromJson α] (k : String) : Except String α

Equations

• j.getObjValAs? α k = Lean.fromJson? (j.getObjValD k)

def Lean.Json.setObjValAs! (j : Lean.Json) {α : Type u} [Lean.ToJson α] (k : String) (v : α) : Lean.Json

Equations

• j.setObjValAs! k v = j.setObjVal! k (Lean.toJson v)

def Lean.Json.opt {α : Type u_1} [Lean.ToJson α] (k : String) : Option α → List (String × Lean.Json)

def Lean.Json.parseTagged (json : Lean.Json) (tag : String) (nFields : Nat) (fieldNames? : Option (Array Lean.Name)) : Except String (Array Lean.Json)

Parses a JSON-encoded structure or inductive constructor. Used mostly by deriving FromJson.