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.

def Parser.Char.ASCII.parseNat.binNum {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Nat

Equations

• Parser.Char.ASCII.parseNat.binNum = do let __discr ← Parser.Char.ASCII.binDigit match __discr with | ⟨n, isLt⟩ => Prod.fst <$> Parser.Char.ASCII.binNum✝ n

def Parser.Char.ASCII.parseNat.octNum {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Nat

Equations

• Parser.Char.ASCII.parseNat.octNum = do let __discr ← Parser.Char.ASCII.octDigit match __discr with | ⟨n, isLt⟩ => Prod.fst <$> Parser.Char.ASCII.octNum✝ n

def Parser.Char.ASCII.parseNat.hexNum {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Nat

Equations

• Parser.Char.ASCII.parseNat.hexNum = do let __discr ← Parser.Char.ASCII.hexDigit match __discr with | ⟨n, isLt⟩ => Prod.fst <$> Parser.Char.ASCII.hexNum✝ n

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.

@[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.

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.