class Lean.FromJson (α : Type u) : Type u

Types that can be decoded from JSON.

Use deriving FromJson to automatically generate an instance. See ToJson for details of auto-generated instances.

• fromJson? : Json → Except String α

class Lean.ToJson (α : Type u) : Type u

Types that can be encoded as JSON.

Use deriving ToJson to automatically generate an instance. The following encoding strategy is employed by auto-generated instances:

• Basic types corresponding to JSON values are encoded as these values.

  • Bool is encoded as true/false.

  • Strings are encoded as JSON strings.

  • Numeric types are encoded as JSON numbers, with the exception of:

    • UInt64 and USize which are encoded as JSON strings. This is because, although JSON numbers proper have unbounded range, in JavaScript they are parsed as Numbers and these can only represent integers up to $2^{53} - 1$ safely; so a roundtrip through JavaScript would result in truncation on these types. (We use these types in the JavaScript-based Lean infoview.)

    • Special Floats which are encoded as JSON strings: "NaN"/"Infinity"/"-Infinity".

• Unit is encoded as {} (empty JSON object).

• Arrays and Lists are encoded as JSON arrays.

• Option.none is encoded as null, whereas some a has the same encoding as a. Note that this implies Option (Option α) does not roundtrip, since none and some none both become null.

• General structures are encoded as JSON objects in the obvious way.

  • Option fields whose names end with ? have special support: the question mark is omitted from the JSON field name, and such a field is omitted from the JSON object when its value is none (as opposed to being encoded as { "someField": null }).

• General inductive types are encoded on a per-constructor basis.

  • An argument-free constructor is encoded as its name (a JSON string).

  • A constructor with named arguments only is encoded as the JSON object { "ctorName": { "arg1": argVal1, ..., "argN": argValN } }.

  • A constructor with one unnamed argument is encoded as the JSON object { "ctorName": argVal }.

  • A constructor with more than one unnamed argument is encoded as the JSON object { "ctorName": [argVal1, ..., argValN] }.

• Certain other types have special handling: see the instances below.

• toJson : α → Json

@[implicit_reducible]

instance Lean.instFromJsonJson : FromJson Json

Equations

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

@[implicit_reducible]

instance Lean.instToJsonJson : ToJson Json

Equations

• Lean.instToJsonJson = { toJson := id }

@[implicit_reducible]

instance Lean.instFromJsonJsonNumber : FromJson JsonNumber

Equations

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

@[implicit_reducible]

instance Lean.instToJsonJsonNumber : ToJson JsonNumber

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonUnit : FromJson Unit

Equations

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

@[implicit_reducible]

instance Lean.instToJsonUnit : ToJson Unit

Equations

• Lean.instToJsonUnit = { toJson := fun (x : Unit) => Lean.Json.obj ∅ }

@[implicit_reducible]

instance Lean.instFromJsonEmpty : FromJson Empty

Equations

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

@[implicit_reducible]

instance Lean.instToJsonEmpty : ToJson Empty

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonBool : FromJson Bool

Equations

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

@[implicit_reducible]

instance Lean.instToJsonBool : ToJson Bool

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonNat : FromJson Nat

Equations

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

@[implicit_reducible]

instance Lean.instToJsonNat : ToJson Nat

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonInt : FromJson Int

Equations

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

@[implicit_reducible]

instance Lean.instToJsonInt : ToJson Int

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonString : FromJson String

Equations

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

@[implicit_reducible]

instance Lean.instToJsonString : ToJson String

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonSlice : FromJson String.Slice

Equations

• Lean.instFromJsonSlice = { fromJson? := Except.map String.toSlice ∘ Lean.Json.getStr? }

@[implicit_reducible]

instance Lean.instToJsonSlice : ToJson String.Slice

Equations

• Lean.instToJsonSlice = { toJson := fun (s : String.Slice) => Lean.Json.str s.copy }

@[implicit_reducible]

instance Lean.instFromJsonFilePath : FromJson System.FilePath

Equations

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

@[implicit_reducible]

instance Lean.instToJsonFilePath : ToJson System.FilePath

Equations

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

def Array.fromJson? {α : Type u_1} [Lean.FromJson α] : Lean.Json → Except String (Array α)

Equations

• Array.fromJson? (Lean.Json.arr a) = Array.mapM Lean.fromJson? a
• Array.fromJson? x✝ = throw (toString "expected JSON array, got '" ++ toString x✝ ++ toString "'")

@[implicit_reducible]

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

Equations

• Lean.instFromJsonArray = { fromJson? := Array.fromJson? }

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

Equations

• a.toJson = Lean.Json.arr (Array.map Lean.toJson a)

@[implicit_reducible]

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

Equations

• Lean.instToJsonArray = { toJson := Array.toJson }

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

Equations

• List.fromJson? j = Except.map Array.toList (Lean.fromJson? j)

@[implicit_reducible]

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

Equations

• Lean.instFromJsonList = { fromJson? := List.fromJson? }

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

Equations

• a.toJson = Lean.toJson a.toArray

@[implicit_reducible]

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

Equations

• Lean.instToJsonList = { toJson := List.toJson }

def Option.fromJson? {α : Type u_1} [Lean.FromJson α] : Lean.Json → Except String (Option α)

Equations

• Option.fromJson? Lean.Json.null = Except.ok none
• Option.fromJson? x✝ = some <$> Lean.fromJson? x✝

@[implicit_reducible]

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

Equations

• Lean.instFromJsonOption = { fromJson? := Option.fromJson? }

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

Equations

• none.toJson = Lean.Json.null
• (some a).toJson = Lean.toJson a

@[implicit_reducible]

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

Equations

• Lean.instToJsonOption = { toJson := Option.toJson }

def Prod.fromJson? {α : Type u} {β : Type v} [Lean.FromJson α] [Lean.FromJson β] : Lean.Json → Except String (α × β)

Equations

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

@[implicit_reducible]

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

Equations

• Lean.instFromJsonProd = { fromJson? := Prod.fromJson? }

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

Equations

• (a, b).toJson = Lean.Json.arr #[Lean.toJson a, Lean.toJson b]

@[implicit_reducible]

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

Equations

• Lean.instToJsonProd = { toJson := Prod.toJson }

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonName : FromJson Name

Equations

• Lean.instFromJsonName = { fromJson? := Lean.Name.fromJson? }

@[implicit_reducible]

instance Lean.instToJsonName : ToJson Name

Equations

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

def Lean.NameMap.fromJson? {α : Type} [FromJson α] : Json → Except String (NameMap α)

Equations

• One or more equations did not get rendered due to their size.
• Lean.NameMap.fromJson? x✝ = throw (toString "expected a `NameMap`, got '" ++ toString x✝ ++ toString "'")

@[implicit_reducible]

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

Equations

• Lean.instFromJsonNameMap = { fromJson? := Lean.NameMap.fromJson? }

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

Equations

• m.toJson = Lean.Json.obj (Std.TreeMap.foldl (fun (n : Std.TreeMap.Raw String Lean.Json compare) (k : Lean.Name) (v : α) => n.insert k.toString (Lean.toJson v)) ∅ m)

@[implicit_reducible]

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

Equations

• Lean.instToJsonNameMap = { toJson := Lean.NameMap.toJson }

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.

def Lean.bignumToJson (n : Nat) : Json

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonUSize : FromJson USize

Equations

• Lean.instFromJsonUSize = { fromJson? := USize.fromJson? }

@[implicit_reducible]

instance Lean.instToJsonUSize : ToJson USize

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.instFromJsonUInt64 : FromJson UInt64

Equations

• Lean.instFromJsonUInt64 = { fromJson? := UInt64.fromJson? }

@[implicit_reducible]

instance Lean.instToJsonUInt64 : ToJson UInt64

Equations

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

def Float.toJson (x : Float) : Lean.Json

Equations

• x.toJson = match Lean.JsonNumber.fromFloat? x with | Sum.inl e => Lean.Json.str e | Sum.inr n => Lean.Json.num n

@[implicit_reducible]

instance Lean.instToJsonFloat : ToJson Float

Equations

• Lean.instToJsonFloat = { toJson := Float.toJson }

def Float.fromJson? : Lean.Json → Except String Float

Equations

• Float.fromJson? (Lean.Json.str "Infinity") = Except.ok (1.0 / 0.0)
• Float.fromJson? (Lean.Json.str "-Infinity") = Except.ok (-1.0 / 0.0)
• Float.fromJson? (Lean.Json.str "NaN") = Except.ok (0.0 / 0.0)
• Float.fromJson? (Lean.Json.num jn) = Except.ok jn.toFloat
• Float.fromJson? x✝ = Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."

@[implicit_reducible]

instance Lean.instFromJsonFloat : FromJson Float

Equations

• Lean.instFromJsonFloat = { fromJson? := Float.fromJson? }

def Lean.Json.Structured.fromJson? : Json → Except String Structured

Equations

• Lean.Json.Structured.fromJson? (Lean.Json.arr a) = pure (Lean.Json.Structured.arr a)
• Lean.Json.Structured.fromJson? (Lean.Json.obj o) = pure (Lean.Json.Structured.obj o)
• Lean.Json.Structured.fromJson? x✝ = throw (toString "expected structured object, got '" ++ toString x✝ ++ toString "'")

@[implicit_reducible]

instance Lean.Json.instFromJsonStructured : FromJson Structured

Equations

• Lean.Json.instFromJsonStructured = { fromJson? := Lean.Json.Structured.fromJson? }

def Lean.Json.Structured.toJson : Structured → Json

Equations

• (Lean.Json.Structured.arr a).toJson = Lean.Json.arr a
• (Lean.Json.Structured.obj o).toJson = Lean.Json.obj o

@[implicit_reducible]

instance Lean.Json.instToJsonStructured : ToJson Structured

Equations

• Lean.Json.instToJsonStructured = { toJson := Lean.Json.Structured.toJson }

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

Equations

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

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

Equations

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

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

Equations

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

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

def Lean.Json.getTag? : Json → Option String

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

Equations

• (Lean.Json.str tag).getTag? = some tag
• (Lean.Json.obj kvs).getTag? = guard ((kvs.size == 1) = true) *> kvs.minKey?
• x✝.getTag? = none

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

Equations

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

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.

Equations

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