Safe Haskell	None
Language	GHC2021

Data.Type.Nat.Singleton

Contents

Synopsis

data SNat (n :: Nat) where
- pattern Z :: () => n ~ 'Z => SNat n
- pattern S :: () => Pos n => SNat (Pred n) -> SNat n
fromSNat :: forall i (n :: Nat). Integral i => SNat n -> i
fromSNatRaw :: forall (n :: Nat). SNat n -> SNatRep
plus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
decSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m)
data SomeSNat = SomeSNat !(SNat n)
withSomeSNat :: (forall (n :: Nat). SNat n -> a) -> SomeSNat -> a
toSomeSNat :: Integral i => i -> SomeSNat
toSomeSNatRaw :: SNatRep -> SomeSNat
fromSomeSNat :: Integral i => SomeSNat -> i
fromSomeSNatRaw :: SomeSNat -> SNatRep
plusUnitL :: forall (n :: Nat). Proxy n -> ('Z + n) :~: n
plusUnitR :: forall (n :: Nat). SNat n -> (n + 'Z) :~: n
plusCommS :: forall (n :: Nat) (m :: Nat). SNat n -> Proxy m -> 'S (n + m) :~: (n + 'S m)
plusComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n + m) :~: (m + n)
plusAssoc :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> Proxy m -> Proxy l -> ((n + m) + l) :~: (n + (m + l))
class KnownNat (n :: Nat) where
- natSing :: SNat n
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
type SNatRep = Int

Natural Number Singletons

data SNat (n :: Nat) where #

Bundled Patterns

pattern Z :: () => n ~ 'Z => SNat n
pattern S :: () => Pos n => SNat (Pred n) -> SNat n

Instances details

Show (SNat n)
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
NFData (SNat n)
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods rnf :: SNat n -> () #
Eq (SNat n)
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #

fromSNat :: forall i (n :: Nat). Integral i => SNat n -> i #

fromSNatRaw :: forall (n :: Nat). SNat n -> SNatRep #

plus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m) #

decSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m) #

Existential Wrapper

Constructors

Instances details

Show SomeSNat
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods showsPrec :: Int -> SomeSNat -> ShowS # show :: SomeSNat -> String # showList :: [SomeSNat] -> ShowS #
NFData SomeSNat
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods rnf :: SomeSNat -> () #
Eq SomeSNat
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods (==) :: SomeSNat -> SomeSNat -> Bool # (/=) :: SomeSNat -> SomeSNat -> Bool #

withSomeSNat :: (forall (n :: Nat). SNat n -> a) -> SomeSNat -> a #

plusUnitL :: forall (n :: Nat). Proxy n -> ('Z + n) :~: n #

plusUnitR :: forall (n :: Nat). SNat n -> (n + 'Z) :~: n #

plusCommS :: forall (n :: Nat) (m :: Nat). SNat n -> Proxy m -> 'S (n + m) :~: (n + 'S m) #

plusComm :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n + m) :~: (m + n) #

plusAssoc :: forall (n :: Nat) (m :: Nat) (l :: Nat). SNat n -> Proxy m -> Proxy l -> ((n + m) + l) :~: (n + (m + l)) #

class KnownNat (n :: Nat) where #

Methods

Instances details

KnownNat 'Z
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods natSing :: SNat 'Z #
KnownNat n => KnownNat ('S n)
Instance details Defined in Data.Type.Nat.Singleton.Fast Methods natSing :: SNat ('S n) #

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r #