Equations
- Lean.JsonNumber.fromNat n = { mantissa := Int.ofNat n, exponent := 0 }
Equations
- Lean.JsonNumber.fromInt n = { mantissa := n, exponent := 0 }
Equations
Equations
Equations
- Lean.JsonNumber.instOfNatJsonNumber = { ofNat := Lean.JsonNumber.fromNat n }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.JsonNumber.ltProp = { lt := fun a b => Lean.JsonNumber.lt a b = true }
instance
Lean.JsonNumber.instDecidableLtJsonNumberInstLTJsonNumber
(a : Lean.JsonNumber)
(b : Lean.JsonNumber)
:
Equations
Equations
- Lean.JsonNumber.instOrdJsonNumber = { compare := fun x y => if x < y then Ordering.lt else if x > y then Ordering.gt else Ordering.eq }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.JsonNumber.shiftr _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { mantissa := m, exponent := e }, s => { mantissa := m, exponent := e + s }
Equations
- Lean.JsonNumber.instToStringJsonNumber = { toString := Lean.JsonNumber.toString }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instInhabitedJson = { default := Lean.Json.null }
Equations
- Lean.Json.instBEqJson = { beq := Lean.Json.beq' }
Equations
- Lean.Json.instCoeNatJson = { coe := fun n => Lean.Json.num (Lean.JsonNumber.fromNat n) }
Equations
- Lean.Json.instCoeIntJson = { coe := fun n => Lean.Json.num (Lean.JsonNumber.fromInt n) }
Equations
- Lean.Json.instCoeStringJson = { coe := Lean.Json.str }
Equations
- Lean.Json.instCoeBoolJson = { coe := Lean.Json.bool }
Equations
- Lean.Json.instOfNatJson = { ofNat := Lean.Json.num (Lean.JsonNumber.fromNat n) }
Equations
- Lean.Json.isNull _fun_discr = match _fun_discr with | Lean.Json.null => true | x => false
Equations
- Lean.Json.getObj? _fun_discr = match _fun_discr with | Lean.Json.obj kvs => pure kvs | x => throw "object expected"
Equations
- Lean.Json.getArr? _fun_discr = match _fun_discr with | Lean.Json.arr a => pure a | x => throw "array expected"
Equations
- Lean.Json.getStr? _fun_discr = match _fun_discr with | Lean.Json.str s => pure s | x => throw "String expected"
Equations
- Lean.Json.getNat? _fun_discr = match _fun_discr with | Lean.Json.num { mantissa := Int.ofNat n, exponent := 0 } => pure n | x => throw "Natural number expected"
Equations
- Lean.Json.getInt? _fun_discr = match _fun_discr with | Lean.Json.num { mantissa := i, exponent := 0 } => pure i | x => throw "Integer expected"
Equations
- Lean.Json.getBool? _fun_discr = match _fun_discr with | Lean.Json.bool b => pure b | x => throw "Bool expected"
Equations
- Lean.Json.getNum? _fun_discr = match _fun_discr with | Lean.Json.num n => pure n | x => throw "number expected"
Equations
- arr: Array Lean.Json → Lean.Json.Structured
- obj: (Std.RBNode String fun x => Lean.Json) → Lean.Json.Structured
Equations
instance
Lean.Json.instCoeRBNodeStringJsonStructured:
Coe (Std.RBNode String fun x => Lean.Json) Lean.Json.Structured