Lean.Data.Json.FromToJson

source

class Lean.FromJson (α : Type u) :

Type u

fromJson? : Json → Except String α

Instances

source

class Lean.ToJson (α : Type u) :

Type u

toJson : α → Json

Instances

source

instance Lean.instFromJsonJson :

FromJson Json

Equations

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

source

instance Lean.instToJsonJson :

ToJson Json

Equations

Lean.instToJsonJson = { toJson := id }

source

instance Lean.instFromJsonJsonNumber :

FromJson JsonNumber

Equations

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

source

instance Lean.instToJsonJsonNumber :

ToJson JsonNumber

Equations

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

source

instance Lean.instFromJsonEmpty :

FromJson Empty

Equations

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

source

instance Lean.instToJsonEmpty :

ToJson Empty

Equations

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

source

instance Lean.instFromJsonBool :

FromJson Bool

Equations

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

source

instance Lean.instToJsonBool :

ToJson Bool

Equations

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

source

instance Lean.instFromJsonNat :

FromJson Nat

Equations

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

source

instance Lean.instToJsonNat :

ToJson Nat

Equations

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

source

instance Lean.instFromJsonInt :

FromJson Int

Equations

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

source

instance Lean.instToJsonInt :

ToJson Int

Equations

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

source

instance Lean.instFromJsonString :

FromJson String

Equations

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

source

instance Lean.instToJsonString :

ToJson String

Equations

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

source

instance Lean.instFromJsonFilePath :

FromJson System.FilePath

Equations

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

source

instance Lean.instToJsonFilePath :

ToJson System.FilePath

Equations

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

source

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

FromJson (Array α)

Equations

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

source

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

ToJson (Array α)

Equations

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

source

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

FromJson (List α)

Equations

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

source

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

ToJson (List α)

Equations

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

source

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

FromJson (Option α)

Equations

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

source

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

ToJson (Option α)

Equations

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

source

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

FromJson (α × β)

Equations

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

source

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

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 :

FromJson Name

Equations

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

source

instance Lean.instToJsonName :

ToJson Name

Equations

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

source

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.

source

def Lean.bignumToJson (n : Nat) :

Json

Equations

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

source

instance Lean.instFromJsonUSize :

FromJson USize

Equations

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

source

instance Lean.instToJsonUSize :

ToJson USize

Equations

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

source

instance Lean.instFromJsonUInt64 :

FromJson UInt64

Equations

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

source

instance Lean.instToJsonUInt64 :

ToJson UInt64

Equations

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

source

instance Lean.instToJsonFloat :

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 }

source

instance Lean.instFromJsonFloat :

FromJson Float

Equations

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

source

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

ToJson (RBMap String α cmp)

Equations

Lean.instToJsonRBMapString = { toJson := fun (m : Lean.RBMap String α cmp) => Lean.Json.obj (Lean.RBNode.map (fun (x : String) => Lean.toJson) m.val) }

source

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

FromJson (RBMap String α cmp)

Equations

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

source

instance Lean.Json.instFromJsonStructured :

FromJson Structured

Equations

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

source

instance Lean.Json.instToJsonStructured :

ToJson Structured

Equations

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

source

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

Except String Structured

Equations

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

source

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

Except String α

Equations

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

source

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

Json

Equations

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

source

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)]

source

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.