Lean.Data.Json.FromToJson

source

class Lean.FromJson (α : Type u) :

Type u

fromJson? : Lean.Json → Except String α

Instances

source

class Lean.ToJson (α : Type u) :

Type u

toJson : α → Lean.Json

Instances

source

instance Lean.instFromJsonJson:

Lean.FromJson Lean.Json

Equations

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

source

instance Lean.instToJsonJson:

Lean.ToJson Lean.Json

Equations

Lean.instToJsonJson = { toJson := id }

source

instance Lean.instFromJsonJsonNumber:

Lean.FromJson Lean.JsonNumber

Equations

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

source

instance Lean.instToJsonJsonNumber:

Lean.ToJson Lean.JsonNumber

Equations

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

source

instance Lean.instFromJsonBool:

Lean.FromJson Bool

Equations

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

source

instance Lean.instToJsonBool:

Lean.ToJson Bool

Equations

Lean.instToJsonBool = { toJson := fun b => Lean.Json.bool b }

source

instance Lean.instFromJsonNat:

Lean.FromJson Nat

Equations

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

source

instance Lean.instToJsonNat:

Lean.ToJson Nat

Equations

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

source

instance Lean.instFromJsonInt:

Lean.FromJson Int

Equations

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

source

instance Lean.instToJsonInt:

Lean.ToJson Int

Equations

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

source

instance Lean.instFromJsonString:

Lean.FromJson String

Equations

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

source

instance Lean.instToJsonString:

Lean.ToJson String

Equations

Lean.instToJsonString = { toJson := fun s => Lean.Json.str s }

source

instance Lean.instFromJsonFilePath:

Lean.FromJson System.FilePath

Equations

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

source

instance Lean.instToJsonFilePath:

Lean.ToJson System.FilePath

Equations

Lean.instToJsonFilePath = { toJson := fun p => Lean.Json.str p.toString }

source

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

Lean.FromJson (Array α)

Equations

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

source

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

Lean.ToJson (Array α)

Equations

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

source

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

Lean.FromJson (List α)

Equations

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

source

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

Lean.ToJson (List α)

Equations

Lean.instToJsonList = { toJson := fun xs => Lean.toJson (List.toArray xs) }

source

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

Lean.FromJson (Option α)

Equations

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

source

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

Lean.ToJson (Option α)

Equations

Lean.instToJsonOption = { toJson := fun x => match x with | none => Lean.Json.null | some a => Lean.toJson a }

source

instance Lean.instFromJsonProd {α : Type (max u_1 u_2)} {β : Type (max u_1 u_2)} [inst : Lean.FromJson α] [inst : Lean.FromJson β] :

Lean.FromJson (α × β)

Equations

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

source

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

Lean.ToJson (α × β)

Equations

Lean.instToJsonProd = { toJson := fun x => match x with | (a, b) => Lean.Json.arr #[Lean.toJson a, Lean.toJson b] }

source

instance Lean.instFromJsonName:

Lean.FromJson Lean.Name

Equations

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

source

instance Lean.instToJsonName:

Lean.ToJson Lean.Name

Equations

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

source

def Lean.bignumFromJson? (j : Lean.Json) :

Except String Nat

Equations

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

source

def Lean.bignumToJson (n : Nat) :

Lean.Json

Equations

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

source

instance Lean.instFromJsonUSize:

Lean.FromJson USize

Equations

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

source

instance Lean.instToJsonUSize:

Lean.ToJson USize

Equations

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

source

instance Lean.instFromJsonUInt64:

Lean.FromJson UInt64

Equations

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

source

instance Lean.instToJsonUInt64:

Lean.ToJson UInt64

Equations

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

source

instance Lean.Json.instFromJsonStructured:

Lean.FromJson Lean.Json.Structured

Equations

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

source

instance Lean.Json.instToJsonStructured:

Lean.ToJson Lean.Json.Structured

Equations

Lean.Json.instToJsonStructured = { toJson := fun x => match x with | Lean.Json.Structured.arr a => Lean.Json.arr a | Lean.Json.Structured.obj o => Lean.Json.obj o }

source

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

Except String Lean.Json.Structured

Equations

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

source

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

Except String α

Equations

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

source

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

Option α → List (String × Lean.Json)

Equations

Lean.Json.opt k _fun_discr = match _fun_discr with | none => [] | some o => [(k, Lean.toJson o)]

source

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.

Equations

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