Lean.Data.Json.Basic

source

structure Lean.JsonNumber :

Type

mantissa : Int
exponent : Nat

Instances For

source

instance Lean.instDecidableEqJsonNumber :

DecidableEq Lean.JsonNumber

Equations

Lean.instDecidableEqJsonNumber = Lean.decEqJsonNumber✝

source

instance Lean.instHashableJsonNumber :

Hashable Lean.JsonNumber

Equations

Lean.instHashableJsonNumber = { hash := Lean.hashJsonNumber✝ }

source

def Lean.JsonNumber.fromNat (n : Nat) :

Lean.JsonNumber

Equations

Lean.JsonNumber.fromNat n = { mantissa := ↑n, exponent := 0 }

source

def Lean.JsonNumber.fromInt (n : Int) :

Lean.JsonNumber

Equations

Lean.JsonNumber.fromInt n = { mantissa := n, exponent := 0 }

source

instance Lean.JsonNumber.instCoeNat :

Coe Nat Lean.JsonNumber

Equations

Lean.JsonNumber.instCoeNat = { coe := Lean.JsonNumber.fromNat }

source

instance Lean.JsonNumber.instCoeInt :

Coe Int Lean.JsonNumber

Equations

Lean.JsonNumber.instCoeInt = { coe := Lean.JsonNumber.fromInt }

source

instance Lean.JsonNumber.instOfNat {n : Nat} :

OfNat Lean.JsonNumber n

Equations

Lean.JsonNumber.instOfNat = { ofNat := Lean.JsonNumber.fromNat n }

source

def Lean.JsonNumber.normalize :

Lean.JsonNumber → Int × Nat × Int

Equations

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

source

def Lean.JsonNumber.lt (a : Lean.JsonNumber) (b : Lean.JsonNumber) :

Bool

Equations

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

source

def Lean.JsonNumber.ltProp :

LT Lean.JsonNumber

Equations

Lean.JsonNumber.ltProp = { lt := fun (a b : Lean.JsonNumber) => a.lt b = true }

source

instance Lean.JsonNumber.instLT :

LT Lean.JsonNumber

Equations

Lean.JsonNumber.instLT = Lean.JsonNumber.ltProp

source

instance Lean.JsonNumber.instDecidableLt (a : Lean.JsonNumber) (b : Lean.JsonNumber) :

Decidable (a < b)

Equations

a.instDecidableLt b = inferInstanceAs (Decidable (a.lt b = true))

source

instance Lean.JsonNumber.instOrd :

Ord Lean.JsonNumber

Equations

Lean.JsonNumber.instOrd = { compare := fun (x y : Lean.JsonNumber) => if x < y then Ordering.lt else if x > y then Ordering.gt else Ordering.eq }

source

def Lean.JsonNumber.toString :

Lean.JsonNumber → String

Equations

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

source

def Lean.JsonNumber.shiftl :

Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

x✝.shiftl x = match x✝, x with | { mantissa := m, exponent := e }, s => { mantissa := m * ↑(10 ^ (s - e)), exponent := e - s }

source

def Lean.JsonNumber.shiftr :

Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

x✝.shiftr x = match x✝, x with | { mantissa := m, exponent := e }, s => { mantissa := m, exponent := e + s }

source

instance Lean.JsonNumber.instToString :

ToString Lean.JsonNumber

Equations

Lean.JsonNumber.instToString = { toString := Lean.JsonNumber.toString }

source

instance Lean.JsonNumber.instRepr :

Repr Lean.JsonNumber

Equations

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

source

instance Lean.JsonNumber.instOfScientific :

OfScientific Lean.JsonNumber

Equations

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

source

instance Lean.JsonNumber.instNeg :

Neg Lean.JsonNumber

Equations

Lean.JsonNumber.instNeg = { neg := fun (jn : Lean.JsonNumber) => { mantissa := -jn.mantissa, exponent := jn.exponent } }

source

instance Lean.JsonNumber.instInhabited :

Inhabited Lean.JsonNumber

Equations

Lean.JsonNumber.instInhabited = { default := 0 }

source

def Lean.JsonNumber.toFloat :

Lean.JsonNumber → Float

Equations

x.toFloat = match x with | { mantissa := m, exponent := e } => (if m ≥ 0 then 1.0 else -1.0) * OfScientific.ofScientific m.natAbs true e

source

def Lean.JsonNumber.fromFloat? (x : Float) :

String ⊕ Lean.JsonNumber

Attempts to convert a float to a JsonNumber, if the number isn't finite returns the appropriate string from "NaN", "Infinity", "-Infinity".

Equations

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

source

def Lean.strLt (a : String) (b : String) :

Bool

Equations

Lean.strLt a b = decide (a < b)

source

inductive Lean.Json :

Type

null: Lean.Json
bool: Bool → Lean.Json
num: Lean.JsonNumber → Lean.Json
str: String → Lean.Json
arr: Array Lean.Json → Lean.Json
obj: (Lean.RBNode String fun (x : String) => Lean.Json) → Lean.Json

Instances For

source

instance Lean.instInhabitedJson :

Inhabited Lean.Json

Equations

Lean.instInhabitedJson = { default := Lean.Json.null }

source

instance Lean.Json.instBEq :

BEq Lean.Json

Equations

Lean.Json.instBEq = { beq := Lean.Json.beq' }

source

instance Lean.Json.instHashable :

Hashable Lean.Json

Equations

Lean.Json.instHashable = { hash := Lean.Json.hash' }

source

def Lean.Json.mkObj (o : List (String × Lean.Json)) :

Lean.Json

Equations

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

source

instance Lean.Json.instCoeNat :

Coe Nat Lean.Json

Equations

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

source

instance Lean.Json.instCoeInt :

Coe Int Lean.Json

Equations

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

source

instance Lean.Json.instCoeString :

Coe String Lean.Json

Equations

Lean.Json.instCoeString = { coe := Lean.Json.str }

source

instance Lean.Json.instCoeBool :

Coe Bool Lean.Json

Equations

Lean.Json.instCoeBool = { coe := Lean.Json.bool }

source

instance Lean.Json.instOfNat {n : Nat} :

OfNat Lean.Json n

Equations

Lean.Json.instOfNat = { ofNat := Lean.Json.num (Lean.JsonNumber.fromNat n) }

source

def Lean.Json.isNull :

Lean.Json → Bool

Equations

x.isNull = match x with | Lean.Json.null => true | x => false

source

def Lean.Json.getObj? :

Lean.Json → Except String (Lean.RBNode String fun (x : String) => Lean.Json)

Equations

x.getObj? = match x with | Lean.Json.obj kvs => pure kvs | x => throw "object expected"

source

def Lean.Json.getArr? :

Lean.Json → Except String (Array Lean.Json)

Equations

x.getArr? = match x with | Lean.Json.arr a => pure a | x => throw "array expected"

source

def Lean.Json.getStr? :

Lean.Json → Except String String

Equations

x.getStr? = match x with | Lean.Json.str s => pure s | x => throw "String expected"

source

def Lean.Json.getNat? :

Lean.Json → Except String Nat

Equations

x.getNat? = match x with | Lean.Json.num { mantissa := Int.ofNat n, exponent := 0 } => pure n | x => throw "Natural number expected"

source

def Lean.Json.getInt? :

Lean.Json → Except String Int

Equations

x.getInt? = match x with | Lean.Json.num { mantissa := i, exponent := 0 } => pure i | x => throw "Integer expected"

source

def Lean.Json.getBool? :

Lean.Json → Except String Bool

Equations

x.getBool? = match x with | Lean.Json.bool b => pure b | x => throw "Bool expected"

source

def Lean.Json.getNum? :

Lean.Json → Except String Lean.JsonNumber

Equations

x.getNum? = match x with | Lean.Json.num n => pure n | x => throw "number expected"

source

def Lean.Json.getObjVal? :

Lean.Json → String → Except String Lean.Json

Equations

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

source

def Lean.Json.getArrVal? :

Lean.Json → Nat → Except String Lean.Json

Equations

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

source

def Lean.Json.getObjValD (j : Lean.Json) (k : String) :

Lean.Json

Equations

j.getObjValD k = (j.getObjVal? k).toOption.getD Lean.Json.null

source

def Lean.Json.setObjVal! :

Lean.Json → String → Lean.Json → Lean.Json

Equations

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

source

def Lean.Json.mergeObj :

Lean.Json → Lean.Json → Lean.Json

Assuming both inputs o₁, o₂ are json objects, will compute {...o₁, ...o₂}. If o₁ is not a json object, o₂ will be returned.

Equations

x✝.mergeObj x = match x✝, x with | Lean.Json.obj kvs₁, Lean.Json.obj kvs₂ => Lean.Json.obj (Lean.RBNode.fold (Lean.RBNode.insert compare) kvs₁ kvs₂) | x, j₂ => j₂

source

inductive Lean.Json.Structured :

Type

arr: Array Lean.Json → Lean.Json.Structured
obj: (Lean.RBNode String fun (x : String) => Lean.Json) → Lean.Json.Structured

Instances For

source

instance Lean.Json.instCoeArrayStructured :

Coe (Array Lean.Json) Lean.Json.Structured

Equations

Lean.Json.instCoeArrayStructured = { coe := Lean.Json.Structured.arr }

source

instance Lean.Json.instCoeRBNodeStringStructured :

Coe (Lean.RBNode String fun (x : String) => Lean.Json) Lean.Json.Structured

Equations

Lean.Json.instCoeRBNodeStringStructured = { coe := Lean.Json.Structured.obj }