Documentation

Lean.Data.Json.FromToJson

class Lean.FromJson (α : Type u) :

fromJson? : Lean.Json → Except String α

Instances

class Lean.ToJson (α : Type u) :

toJson : α → Lean.Json

Instances

instance Lean.instFromJsonJson :

Lean.FromJson Lean.Json

instance Lean.instToJsonJson :

Lean.ToJson Lean.Json

instance Lean.instFromJsonJsonNumber :

Lean.FromJson Lean.JsonNumber

instance Lean.instToJsonJsonNumber :

Lean.ToJson Lean.JsonNumber

instance Lean.instFromJsonBool :

Lean.FromJson Bool

instance Lean.instToJsonBool :

Lean.ToJson Bool

instance Lean.instFromJsonNat :

Lean.FromJson Nat

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

instance Lean.instFromJsonFilePath :

Lean.FromJson Lake.FilePath

instance Lean.instToJsonFilePath :

Lean.ToJson Lake.FilePath

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

Lean.FromJson (Array α)

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

Lean.ToJson (Array α)

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

Lean.FromJson (List α)

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

Lean.ToJson (List α)

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

Lean.FromJson (Option α)

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

Lean.ToJson (Option α)

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

Lean.FromJson (α × β)

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

Lean.ToJson (α × β)

instance Lean.instFromJsonName :

Lean.FromJson Lake.Name

instance Lean.instToJsonName :

Lean.ToJson Lake.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.

Instances For

def Lean.bignumToJson (n : Nat) :

Instances For

instance Lean.instFromJsonUSize :

Lean.FromJson USize

instance Lean.instToJsonUSize :

Lean.ToJson USize

instance Lean.instFromJsonUInt64 :

Lean.FromJson UInt64

instance Lean.instToJsonUInt64 :

Lean.ToJson UInt64

instance Lean.instToJsonFloat :

Lean.ToJson Float

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)

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

Instances For

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

Except String α

Instances For

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

Instances For

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

Option α → List (String × Lean.Json)

Instances For

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

Except String (Array Lean.Json)

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

Instances For