Documentation

Parser.Char.Numeric

source
def Parser.Char.ASCII.parseNat {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (decimalOnly : Bool := true) :
ParserT ε σ Char m Nat

Parse a Nat

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Parser.Char.ASCII.parseInt {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (decimalOnly : Bool := true) :
    ParserT ε σ Char m Int

    Parse an Int

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[inline]
      def Parser.Char.ASCII.parseScientific {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (α : Type) [OfScientific α] :
      ParserT ε σ Char m α

      Parse scientific notation

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Parser.Char.ASCII.parseFloat {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] :
        ParserT ε σ Char m Float

        Parse a Float

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For