Lean.Data.Json.FromToJson

Lean.instFromJsonArray = { fromJson? := fun x => match x with | Lean.Json.arr a => Array.mapM Lean.fromJson? a | j => throw (toString "expected JSON array, got '" ++ toString j ++ toString "'") }

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

Lean.instFromJsonProd = { fromJson? := fun x => match x with | Lean.Json.arr #[ja, jb] => do let a ← Lean.fromJson? ja let b ← Lean.fromJson? jb pure (a, b) | j => throw (toString "expected pair, got '" ++ toString j ++ toString "'") }

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

Lean.instFromJsonName = { fromJson? := fun j => do let s ← Lean.Json.getStr? j if (s == "[anonymous]") = true then pure Lean.Name.anonymous else do let discr ← pure (Lean.Syntax.decodeNameLit ("`" ++ s)) match discr with | some n => pure n | x => throw (toString "expected a `Name`, got '" ++ toString j ++ toString "'") }

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

Lean.bignumFromJson? j = do let s ← Lean.Json.getStr? j let discr ← pure (Lean.Syntax.decodeNatLitVal? s) match discr with | some v => pure v | x => throw (toString "expected a string-encoded number, got '" ++ toString j ++ toString "'")

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

Lean.instFromJsonUSize = { fromJson? := fun j => do let n ← Lean.bignumFromJson? j let _do_jp : PUnit → Except String USize := fun y => pure (USize.ofNat n) if n ≥ USize.size then do let y ← throw "value '{j}' is too large for `USize`" _do_jp y else do let y ← pure PUnit.unit _do_jp y }

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

Lean.instFromJsonUInt64 = { fromJson? := fun j => do let n ← Lean.bignumFromJson? j let _do_jp : PUnit → Except String UInt64 := fun y => pure (UInt64.ofNat n) if n ≥ UInt64.size then do let y ← throw "value '{j}' is too large for `UInt64`" _do_jp y else do let y ← pure PUnit.unit _do_jp y }