Documentation

Lean.Data.Json.FromToJson.Basic

class Lean.FromJson (α : Type u) :

fromJson? : Json → Except String α

Instances

class Lean.ToJson (α : Type u) :

toJson : α → Json

Instances

@[implicit_reducible]

instance Lean.instFromJsonJson :

@[implicit_reducible]

instance Lean.instToJsonJson :

@[implicit_reducible]

instance Lean.instFromJsonJsonNumber :

FromJson JsonNumber

@[implicit_reducible]

instance Lean.instToJsonJsonNumber :

ToJson JsonNumber

@[implicit_reducible]

instance Lean.instFromJsonEmpty :

@[implicit_reducible]

instance Lean.instToJsonEmpty :

@[implicit_reducible]

instance Lean.instFromJsonBool :

@[implicit_reducible]

instance Lean.instToJsonBool :

@[implicit_reducible]

instance Lean.instFromJsonNat :

@[implicit_reducible]

instance Lean.instToJsonNat :

@[implicit_reducible]

instance Lean.instFromJsonInt :

@[implicit_reducible]

instance Lean.instToJsonInt :

@[implicit_reducible]

instance Lean.instFromJsonString :

FromJson String

@[implicit_reducible]

instance Lean.instToJsonString :

@[implicit_reducible]

instance Lean.instFromJsonSlice :

FromJson String.Slice

@[implicit_reducible]

instance Lean.instToJsonSlice :

ToJson String.Slice

@[implicit_reducible]

instance Lean.instFromJsonFilePath :

FromJson System.FilePath

@[implicit_reducible]

instance Lean.instToJsonFilePath :

ToJson System.FilePath

def Array.fromJson? {α : Type u_1} [Lean.FromJson α] :

Lean.Json → Except String (Array α)

Instances For

@[implicit_reducible]

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

FromJson (Array α)

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

Instances For

@[implicit_reducible]

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

ToJson (Array α)

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

Except String (List α)

Instances For

@[implicit_reducible]

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

FromJson (List α)

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

Instances For

@[implicit_reducible]

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

ToJson (List α)

def Option.fromJson? {α : Type u_1} [Lean.FromJson α] :

Lean.Json → Except String (Option α)

Instances For

@[implicit_reducible]

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

FromJson (Option α)

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

Option α → Lean.Json

Instances For

@[implicit_reducible]

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

ToJson (Option α)

def Prod.fromJson? {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] :

Lean.Json → Except String (α × β)

Instances For

@[implicit_reducible]

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

FromJson (α × β)

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

α × β → Lean.Json

Instances For

@[implicit_reducible]

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

ToJson (α × β)

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

Except String Name

Instances For

@[implicit_reducible]

instance Lean.instFromJsonName :

@[implicit_reducible]

instance Lean.instToJsonName :

def Lean.NameMap.fromJson? {α : Type} [FromJson α] :

Json → Except String (NameMap α)

Instances For

@[implicit_reducible]

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

FromJson (NameMap α)

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

Instances For

@[implicit_reducible]

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

ToJson (NameMap α)

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

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

Except String USize

Instances For

@[implicit_reducible]

instance Lean.instFromJsonUSize :

@[implicit_reducible]

instance Lean.instToJsonUSize :

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

Except String UInt64

Instances For

@[implicit_reducible]

instance Lean.instFromJsonUInt64 :

FromJson UInt64

@[implicit_reducible]

instance Lean.instToJsonUInt64 :

def Float.toJson (x : Float) :

Instances For

@[implicit_reducible]

instance Lean.instToJsonFloat :

def Float.fromJson? :

Lean.Json → Except String Float

Instances For

@[implicit_reducible]

instance Lean.instFromJsonFloat :

def Lean.Json.Structured.fromJson? :

Json → Except String Structured

Instances For

@[implicit_reducible]

instance Lean.Json.instFromJsonStructured :

FromJson Structured

def Lean.Json.Structured.toJson :

Structured → Json

Instances For

@[implicit_reducible]

instance Lean.Json.instToJsonStructured :

ToJson Structured

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

Except String Structured

Instances For

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

Except String α

Instances For

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

Instances For

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

Option α → List (String × Json)

Instances For

def Lean.Json.getTag? :

Json → Option String

Returns the string value or single key name, if any.

Instances For

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

Except String (Array Json)

Instances For

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

Except String (Array Json)

Parses a JSON-encoded structure or inductive constructor, assuming the tag has already been checked and nFields is nonzero. Used mostly by deriving FromJson.

Instances For