Safe Haskell	None
Language	GHC2021

TypeLevelShow.Natural

Description

Turn type-level Naturals into Symbols.

Warning: GHC may error out if you pass an SNat that's too large to the singled functions, due to reduction stack size. Follow the error message instructions if you think you need it. This seems not to happen with :k!, probably due to different settings.

Synopsis

type ShowNatBin (n :: Natural) = ShowNatBase 2 ShowNatDigitHexLowerSym n
type ShowNatOct (n :: Natural) = ShowNatBase 8 ShowNatDigitHexLowerSym n
type ShowNatDec (n :: Natural) = ShowNatBase 10 ShowNatDigitHexLowerSym n
type ShowNatHexLower (n :: Natural) = ShowNatBase 16 ShowNatDigitHexLowerSym n
type ShowNatHexUpper (n :: Natural) = ShowNatBase 16 ShowNatDigitHexUpperSym n
sShowNatBin :: forall (n :: Nat). SNat n -> SSymbol (ShowNatBin n)
sShowNatOct :: forall (n :: Nat). SNat n -> SSymbol (ShowNatOct n)
sShowNatDec :: forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatHexLower :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexLower n)
sShowNatHexUpper :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexUpper n)
type family ShowNatBase (base :: Natural) (showDigit :: Natural ~> Char) (n :: Natural) :: Symbol where ...
sShowNatBase :: forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat). SNat base -> Lam SNat SChar showDigit -> SNat n -> SSymbol (ShowNatBase base showDigit n)
type family ShowNatBase' (base :: Natural) (showDigit :: Natural ~> Char) (acc :: Symbol) (n :: Natural) :: Symbol where ...
sShowNatBase' :: forall (base :: Nat) (showDigit :: Nat ~> Char) (acc :: Symbol) (n :: Nat). SNat base -> Lam SNat SChar showDigit -> SSymbol acc -> SNat n -> SSymbol (ShowNatBase' base showDigit acc n)

Documentation

type ShowNatBin (n :: Natural) = ShowNatBase 2 ShowNatDigitHexLowerSym n Source #

type ShowNatOct (n :: Natural) = ShowNatBase 8 ShowNatDigitHexLowerSym n Source #

type ShowNatDec (n :: Natural) = ShowNatBase 10 ShowNatDigitHexLowerSym n Source #

type ShowNatHexLower (n :: Natural) = ShowNatBase 16 ShowNatDigitHexLowerSym n Source #

type ShowNatHexUpper (n :: Natural) = ShowNatBase 16 ShowNatDigitHexUpperSym n Source #

sShowNatBin :: forall (n :: Nat). SNat n -> SSymbol (ShowNatBin n) Source #

sShowNatOct :: forall (n :: Nat). SNat n -> SSymbol (ShowNatOct n) Source #

sShowNatDec :: forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n) Source #

sShowNatHexLower :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexLower n) Source #

sShowNatHexUpper :: forall (n :: Nat). SNat n -> SSymbol (ShowNatHexUpper n) Source #

type family ShowNatBase (base :: Natural) (showDigit :: Natural ~> Char) (n :: Natural) :: Symbol where ... Source #

Render a type-level Natural in the given base using the given digit renderer.

The digit renderer is guaranteed to be called with 0 <= n < base.

Equations

ShowNatBase base showDigit 0 = "0"
ShowNatBase base showDigit n = ShowNatBase' base showDigit "" n

sShowNatBase :: forall (base :: Nat) (showDigit :: Nat ~> Char) (n :: Nat). SNat base -> Lam SNat SChar showDigit -> SNat n -> SSymbol (ShowNatBase base showDigit n) Source #

type family ShowNatBase' (base :: Natural) (showDigit :: Natural ~> Char) (acc :: Symbol) (n :: Natural) :: Symbol where ... Source #

Equations

ShowNatBase' base showDigit acc 0 = acc
ShowNatBase' base showDigit acc n = ShowNatBase' base showDigit (ConsSymbol (showDigit @@ Mod n base) acc) (Div n base)

sShowNatBase' :: forall (base :: Nat) (showDigit :: Nat ~> Char) (acc :: Symbol) (n :: Nat). SNat base -> Lam SNat SChar showDigit -> SSymbol acc -> SNat n -> SSymbol (ShowNatBase' base showDigit acc n) Source #