Documentation

Lean.Data.Json.Parser

source
def Lean.Json.Parser.hexChar :
Std.Internal.Parsec.String.Parser UInt16
Equations
    Instances For
      source
      def Lean.Json.Parser.finishSurrogatePair (low : UInt16) :
      Std.Internal.Parsec.String.Parser Char
      Equations
        Instances For
          source
          def Lean.Json.Parser.escapedChar :
          Std.Internal.Parsec.String.Parser Char
          Equations
            Instances For
              source
              partial def Lean.Json.Parser.strCore (acc : String) :
              Std.Internal.Parsec.String.Parser String
              source
              @[inline]
              def Lean.Json.Parser.str :
              Std.Internal.Parsec.String.Parser String
              Equations
                Instances For
                  source
                  partial def Lean.Json.Parser.natCore (acc : Nat) :
                  Std.Internal.Parsec.String.Parser Nat
                  source
                  partial def Lean.Json.Parser.natCoreNumDigits (acc digits : Nat) :
                  Std.Internal.Parsec.String.Parser (Nat × Nat)
                  source
                  @[inline]
                  def Lean.Json.Parser.lookahead (p : Char → Prop) (desc : String) [DecidablePred p] :
                  Std.Internal.Parsec.String.Parser Unit
                  Equations
                    Instances For
                      source
                      @[inline]
                      def Lean.Json.Parser.natNonZero :
                      Std.Internal.Parsec.String.Parser Nat
                      Equations
                        Instances For
                          source
                          @[inline]
                          def Lean.Json.Parser.natNumDigits :
                          Std.Internal.Parsec.String.Parser (Nat × Nat)
                          Equations
                            Instances For
                              source
                              @[inline]
                              def Lean.Json.Parser.natMaybeZero :
                              Std.Internal.Parsec.String.Parser Nat
                              Equations
                                Instances For
                                  source
                                  @[inline]
                                  def Lean.Json.Parser.numSign :
                                  Std.Internal.Parsec.String.Parser Int
                                  Equations
                                    Instances For
                                      source
                                      @[inline]
                                      def Lean.Json.Parser.nat :
                                      Std.Internal.Parsec.String.Parser Nat
                                      Equations
                                        Instances For
                                          source
                                          @[inline]
                                          def Lean.Json.Parser.numWithDecimals :
                                          Std.Internal.Parsec.String.Parser JsonNumber
                                          Equations
                                            Instances For
                                              source
                                              @[inline]
                                              def Lean.Json.Parser.exponent (value : JsonNumber) :
                                              Std.Internal.Parsec.String.Parser JsonNumber
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Json.Parser.num :
                                                  Std.Internal.Parsec.String.Parser JsonNumber
                                                  Equations
                                                    Instances For
                                                      source
                                                      partial def Lean.Json.Parser.arrayCore (acc : Array Json) :
                                                      Std.Internal.Parsec.String.Parser (Array Json)
                                                      source
                                                      partial def Lean.Json.Parser.objectCore (kvs : RBNode String fun (x : String) => Json) :
                                                      Std.Internal.Parsec.String.Parser (RBNode String fun (x : String) => Json)
                                                      source
                                                      partial def Lean.Json.Parser.anyCore :
                                                      Std.Internal.Parsec.String.Parser Json
                                                      source
                                                      def Lean.Json.Parser.any :
                                                      Std.Internal.Parsec.String.Parser Json
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Json.parse (s : String) :
                                                          Except String Json
                                                          Equations
                                                            Instances For