SNatI n => GShow (PosP' n)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Bounded (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
Eq (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
Ord (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
SNatI n => Show (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
NFData (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Arbitrary (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
SNatI n => CoArbitrary (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP
(SNatI n, SBinPI b) => Function (PosP' n b)Defined in bin-0.1.4.1 · Data.BinP.PosP

Top & Pop

valuetop :: SBinPI b => PosP b

top and pop serve as FZ and FS, with types specified so type-inference works backwards from the result.

Example1 expression

>>> top :: PosP BinP40

Example1 expression

>>> pop (pop top) :: PosP BinP42

Example1 expression

>>> pop (pop top) :: PosP BinP92

valuepop :: (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b

See top.

Showing

valueexplicitShow :: PosP b -> String

valueexplicitShow' :: PosP' n b -> String

valueexplicitShowsPrec :: Int -> PosP b -> ShowS

valueexplicitShowsPrec' :: Int -> PosP' n b -> ShowS

valuetoNatural :: PosP b -> Natural

Convert PosP to Natural.

valuetoNatural' :: SNatI n => PosP' n b -> Natural

Convert PosP' to Natural.

valueboring :: PosP 'BE

Counting to one is boring

Example1 expression

>>> boring0

valueweakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)

valueweakenRight1' :: SBinP b -> PosP' n b -> PosP' n (Succ b)

valueuniverse :: SBinPI b => [PosP b]

Example1 expression

>>> universe :: [PosP BinP9][0,1,2,3,4,5,6,7,8]

valueuniverse' :: (SNatI n, SBinPI b) => [PosP' n b]

This gives a hint, what the n parameter means in PosP'.

Example1 expression

>>> universe' :: [PosP' N.Nat2 BinP2][0,1,2,3,4,5,6,7]