Documentation

Lean.Data.Json.Basic

structure Lean.JsonNumber:
Type
Equations
Equations
Equations
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
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lean.JsonNumber.shiftl _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { mantissa := m, exponent := e }, s => { mantissa := m * Int.ofNat (10 ^ (s - e)), exponent := e - s }
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
  • One or more equations did not get rendered due to their size.
def Lean.strLt (a : String) (b : String) :
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
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
  • One or more equations did not get rendered due to their size.