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

• fromJson? : Json → Except String α

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

• toJson : α → Json

instance Lean.instFromJsonJson : FromJson Json

Equations

• Lean.instFromJsonJson = { fromJson? := Except.ok }

instance Lean.instToJsonJson : ToJson Json

Equations

• Lean.instToJsonJson = { toJson := id }

instance Lean.instFromJsonJsonNumber : FromJson JsonNumber

Equations

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

instance Lean.instToJsonJsonNumber : ToJson JsonNumber

Equations

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

instance Lean.instFromJsonEmpty : FromJson Empty

Equations

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

instance Lean.instToJsonEmpty : ToJson Empty

Equations

• Lean.instToJsonEmpty = { toJson := fun (a : Empty) => nomatch a }

instance Lean.instFromJsonBool : FromJson Bool

Equations

• Lean.instFromJsonBool = { fromJson? := Lean.Json.getBool? }

instance Lean.instToJsonBool : ToJson Bool

Equations

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

instance Lean.instFromJsonNat : FromJson Nat

Equations

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

instance Lean.instToJsonNat : ToJson Nat

Equations

• Lean.instToJsonNat = { toJson := fun (n : Nat) => Lean.Json.num (Lean.JsonNumber.fromNat n) }

instance Lean.instFromJsonInt : FromJson Int

Equations

• Lean.instFromJsonInt = { fromJson? := Lean.Json.getInt? }

instance Lean.instToJsonInt : ToJson Int

Equations

• Lean.instToJsonInt = { toJson := fun (n : Int) => Lean.Json.num (Lean.JsonNumber.fromInt n) }

instance Lean.instFromJsonString : FromJson String

Equations

• Lean.instFromJsonString = { fromJson? := Lean.Json.getStr? }

instance Lean.instToJsonString : ToJson String

Equations

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

instance Lean.instFromJsonFilePath : FromJson System.FilePath

Equations

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

instance Lean.instToJsonFilePath : ToJson System.FilePath

Equations

• Lean.instToJsonFilePath = { toJson := fun (p : System.FilePath) => Lean.Json.str p.toString }

def Array.fromJson? {α : Type u_1} [Lean.FromJson α] : Lean.Json → Except String (Array α)

Equations

• Array.fromJson? (Lean.Json.arr a) = Array.mapM Lean.fromJson? a
• Array.fromJson? x✝ = throw (toString "expected JSON array, got '" ++ toString x✝ ++ toString "'")

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

Equations

• Lean.instFromJsonArray = { fromJson? := Array.fromJson? }

def Array.toJson {α : Type u_1} [Lean.ToJson α] (a : Array α) : Lean.Json

Equations

• a.toJson = Lean.Json.arr (Array.map Lean.toJson a)

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

Equations

• Lean.instToJsonArray = { toJson := Array.toJson }

def List.fromJson? {α : Type u_1} [Lean.FromJson α] (j : Lean.Json) : Except String (List α)

Equations

• List.fromJson? j = Except.map Array.toList (Lean.fromJson? j)

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

Equations

• Lean.instFromJsonList = { fromJson? := List.fromJson? }

def List.toJson {α : Type u_1} [Lean.ToJson α] (a : List α) : Lean.Json

Equations

• a.toJson = Lean.toJson a.toArray

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

Equations

• Lean.instToJsonList = { toJson := List.toJson }

def Option.fromJson? {α : Type u_1} [Lean.FromJson α] : Lean.Json → Except String (Option α)

Equations

• Option.fromJson? Lean.Json.null = Except.ok none
• Option.fromJson? x✝ = some <$> Lean.fromJson? x✝

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

Equations

• Lean.instFromJsonOption = { fromJson? := Option.fromJson? }

def Option.toJson {α : Type u_1} [Lean.ToJson α] : Option α → Lean.Json

Equations

• none.toJson = Lean.Json.null
• (some a).toJson = Lean.toJson a

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

Equations

• Lean.instToJsonOption = { toJson := Option.toJson }

def Prod.fromJson? {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] : Lean.Json → Except String (α × β)

Equations

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

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

Equations

• Lean.instFromJsonProd = { fromJson? := Prod.fromJson? }

def Prod.toJson {α : Type u_1} {β : Type u_2} [Lean.ToJson α] [Lean.ToJson β] : α × β → Lean.Json

Equations

• (a, b).toJson = Lean.Json.arr #[Lean.toJson a, Lean.toJson b]

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

Equations

• Lean.instToJsonProd = { toJson := Prod.toJson }

def Lean.Name.fromJson? (j : Json) : Except String Name

Equations

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

instance Lean.instFromJsonName : FromJson Name

Equations

• Lean.instFromJsonName = { fromJson? := Lean.Name.fromJson? }

instance Lean.instToJsonName : ToJson Name

Equations

• Lean.instToJsonName = { toJson := fun (n : Lean.Name) => Lean.Json.str (toString n) }

def Lean.NameMap.fromJson? {α : Type} [FromJson α] : Json → Except String (NameMap α)

Equations

• One or more equations did not get rendered due to their size.
• Lean.NameMap.fromJson? x✝ = throw (toString "expected a `NameMap`, got '" ++ toString x✝ ++ toString "'")

instance Lean.instFromJsonNameMap {α : Type} [FromJson α] : FromJson (NameMap α)

Equations

• Lean.instFromJsonNameMap = { fromJson? := Lean.NameMap.fromJson? }

def Lean.NameMap.toJson {α : Type} [ToJson α] (m : NameMap α) : Json

Equations

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

instance Lean.instToJsonNameMap {α : Type} [ToJson α] : ToJson (NameMap α)

Equations

• Lean.instToJsonNameMap = { toJson := Lean.NameMap.toJson }

def Lean.bignumFromJson? (j : 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) : Json

Equations

• Lean.bignumToJson n = Lean.Json.str (toString n)

def USize.fromJson? (j : Lean.Json) : Except String USize

Equations

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

instance Lean.instFromJsonUSize : FromJson USize

Equations

• Lean.instFromJsonUSize = { fromJson? := USize.fromJson? }

instance Lean.instToJsonUSize : ToJson USize

Equations

• Lean.instToJsonUSize = { toJson := fun (v : USize) => Lean.bignumToJson v.toNat }

def UInt64.fromJson? (j : Lean.Json) : Except String UInt64

Equations

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

instance Lean.instFromJsonUInt64 : FromJson UInt64

Equations

• Lean.instFromJsonUInt64 = { fromJson? := UInt64.fromJson? }

instance Lean.instToJsonUInt64 : ToJson UInt64

Equations

• Lean.instToJsonUInt64 = { toJson := fun (v : UInt64) => Lean.bignumToJson v.toNat }

def Float.toJson (x : Float) : Lean.Json

Equations

• x.toJson = match Lean.JsonNumber.fromFloat? x with | Sum.inl e => Lean.Json.str e | Sum.inr n => Lean.Json.num n

instance Lean.instToJsonFloat : ToJson Float

Equations

• Lean.instToJsonFloat = { toJson := Float.toJson }

def Float.fromJson? : Lean.Json → Except String Float

Equations

• Float.fromJson? (Lean.Json.str "Infinity") = Except.ok (1.0 / 0.0)
• Float.fromJson? (Lean.Json.str "-Infinity") = Except.ok (-1.0 / 0.0)
• Float.fromJson? (Lean.Json.str "NaN") = Except.ok (0.0 / 0.0)
• Float.fromJson? (Lean.Json.num jn) = Except.ok jn.toFloat
• Float.fromJson? x✝ = Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."

instance Lean.instFromJsonFloat : FromJson Float

Equations

• Lean.instFromJsonFloat = { fromJson? := Float.fromJson? }

def Lean.RBMap.toJson {α : Type} {cmp : String → String → Ordering} [ToJson α] (m : RBMap String α cmp) : Json

Equations

• m.toJson = Lean.Json.obj (Lean.RBNode.map (fun (x : String) => Lean.toJson) m.val)

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

Equations

• Lean.instToJsonRBMapString = { toJson := Lean.RBMap.toJson }

def Lean.RBMap.fromJson? {α : Type} {cmp : String → String → Ordering} [FromJson α] (j : Json) : Except String (RBMap String α cmp)

Equations

• Lean.RBMap.fromJson? j = do let o ← j.getObj? Lean.RBNode.foldM (fun (x : Lean.RBMap String α cmp) (k : String) (v : Lean.Json) => x.insert k <$> Lean.fromJson? v) ∅ o

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

Equations

• Lean.instFromJsonRBMapString = { fromJson? := Lean.RBMap.fromJson? }

def Lean.Json.Structured.fromJson? : Json → Except String Structured

Equations

• Lean.Json.Structured.fromJson? (Lean.Json.arr a) = pure (Lean.Json.Structured.arr a)
• Lean.Json.Structured.fromJson? (Lean.Json.obj o) = pure (Lean.Json.Structured.obj o)
• Lean.Json.Structured.fromJson? x✝ = throw (toString "expected structured object, got '" ++ toString x✝ ++ toString "'")

instance Lean.Json.instFromJsonStructured : FromJson Structured

Equations

• Lean.Json.instFromJsonStructured = { fromJson? := Lean.Json.Structured.fromJson? }

def Lean.Json.Structured.toJson : Structured → Json

Equations

• (Lean.Json.Structured.arr a).toJson = Lean.Json.arr a
• (Lean.Json.Structured.obj o).toJson = Lean.Json.obj o

instance Lean.Json.instToJsonStructured : ToJson Structured

Equations

• Lean.Json.instToJsonStructured = { toJson := Lean.Json.Structured.toJson }

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

Equations

• Lean.Json.toStructured? v = Lean.fromJson? (Lean.toJson v)

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

Equations

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

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

Equations

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

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

Equations

• Lean.Json.opt k none = []
• Lean.Json.opt k (some a) = [(k, Lean.toJson a)]

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

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

Equations

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