Documentation

Lean.Data.Json.Parser

source
def Lean.Json.Parser.hexChar :
Std.Internal.Parsec.String.Parser UInt16
Instances For
    source
    def Lean.Json.Parser.finishSurrogatePair (low : UInt16) :
    Std.Internal.Parsec.String.Parser Char
    Instances For
      source
      def Lean.Json.Parser.escapedChar :
      Std.Internal.Parsec.String.Parser Char
      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
        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
          Instances For
            source
            @[inline]
            def Lean.Json.Parser.natNonZero :
            Std.Internal.Parsec.String.Parser Nat
            Instances For
              source
              @[inline]
              def Lean.Json.Parser.natNumDigits :
              Std.Internal.Parsec.String.Parser (Nat × Nat)
              Instances For
                source
                @[inline]
                def Lean.Json.Parser.natMaybeZero :
                Std.Internal.Parsec.String.Parser Nat
                Instances For
                  source
                  @[inline]
                  def Lean.Json.Parser.numSign :
                  Std.Internal.Parsec.String.Parser Int
                  Instances For
                    source
                    @[inline]
                    def Lean.Json.Parser.nat :
                    Std.Internal.Parsec.String.Parser Nat
                    Instances For
                      source
                      @[inline]
                      def Lean.Json.Parser.numWithDecimals :
                      Std.Internal.Parsec.String.Parser JsonNumber
                      Instances For
                        source
                        @[inline]
                        def Lean.Json.Parser.exponent (value : JsonNumber) :
                        Std.Internal.Parsec.String.Parser JsonNumber
                        Instances For
                          source
                          def Lean.Json.Parser.num :
                          Std.Internal.Parsec.String.Parser JsonNumber
                          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 : Std.TreeMap.Raw String Json compare) :
                            Std.Internal.Parsec.String.Parser (Std.TreeMap.Raw String Json compare)
                            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
                            Instances For
                              source
                              def Lean.Json.parse (s : String) :
                              Except String Json

                              Parses a JSON value, surrounded by optional whitespace. Objects with duplicate keys are rejected.

                              Instances For