Data.BinP.PosP

Documentation

newtype PosP (b :: BinP)

PosP is to BinP is what Fin is to Nat, when n is Z.

Constructors

PosP

Fields

• unPosP :: PosP' Z b

Instances

SBinPI b => Bounded (PosP b)

Defined in Data.BinP.PosP

Methods

minBound :: PosP b

maxBound :: PosP b

Eq (PosP b)

Defined in Data.BinP.PosP

Methods

(==) :: PosP b -> PosP b -> Bool

(/=) :: PosP b -> PosP b -> Bool

Ord (PosP b)

Defined in Data.BinP.PosP

Methods

compare :: PosP b -> PosP b -> Ordering

(<) :: PosP b -> PosP b -> Bool

(<=) :: PosP b -> PosP b -> Bool

(>) :: PosP b -> PosP b -> Bool

(>=) :: PosP b -> PosP b -> Bool

max :: PosP b -> PosP b -> PosP b

min :: PosP b -> PosP b -> PosP b

Show (PosP b)

Defined in Data.BinP.PosP

Methods

showsPrec :: Int -> PosP b -> ShowS

show :: PosP b -> String

showList :: [PosP b] -> ShowS

SBinPI b => Function (PosP b)

Defined in Data.BinP.PosP

Methods

function :: (PosP b -> b0) -> PosP b :-> b0

SBinPI b => Arbitrary (PosP b)

Defined in Data.BinP.PosP

Methods

arbitrary :: Gen (PosP b)

shrink :: PosP b -> [PosP b]

CoArbitrary (PosP b)

Defined in Data.BinP.PosP

Methods

coarbitrary :: PosP b -> Gen b0 -> Gen b0

data PosP' (n :: Nat) (b :: BinP) where

PosP' is a structure inside PosP.

Constructors

AtEnd

Fields

• :: Wrd n
• -> PosP' n BE

  position is either at the last digit;

Here

Fields

• :: Wrd n
• -> PosP' n (B1 b)

  somewhere here

There1

Fields

• :: PosP' (S n) b
• -> PosP' n (B1 b)

  or there, if the bit is one;

There0

Fields

• :: PosP' (S n) b
• -> PosP' n (B0 b)

  or only there if it is none.

Instances

(SNatI n, SBinPI b) => Bounded (PosP' n b)

Defined in Data.BinP.PosP

Methods

minBound :: PosP' n b

maxBound :: PosP' n b

Eq (PosP' n b)

Defined in Data.BinP.PosP

Methods

(==) :: PosP' n b -> PosP' n b -> Bool

(/=) :: PosP' n b -> PosP' n b -> Bool

Ord (PosP' n b)

Defined in Data.BinP.PosP

Methods

compare :: PosP' n b -> PosP' n b -> Ordering

(<) :: PosP' n b -> PosP' n b -> Bool

(<=) :: PosP' n b -> PosP' n b -> Bool

(>) :: PosP' n b -> PosP' n b -> Bool

(>=) :: PosP' n b -> PosP' n b -> Bool

max :: PosP' n b -> PosP' n b -> PosP' n b

min :: PosP' n b -> PosP' n b -> PosP' n b

SNatI n => Show (PosP' n b)

Defined in Data.BinP.PosP

Methods

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

show :: PosP' n b -> String

showList :: [PosP' n b] -> ShowS

(SNatI n, SBinPI b) => Function (PosP' n b)

Defined in Data.BinP.PosP

Methods

function :: (PosP' n b -> b0) -> PosP' n b :-> b0

(SNatI n, SBinPI b) => Arbitrary (PosP' n b)

Defined in Data.BinP.PosP

Methods

arbitrary :: Gen (PosP' n b)

shrink :: PosP' n b -> [PosP' n b]

SNatI n => CoArbitrary (PosP' n b)

Defined in Data.BinP.PosP

Methods

coarbitrary :: PosP' n b -> Gen b0 -> Gen b0

Top & Pop

top :: SBinPI b => PosP b

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

>>> top :: PosP BinP4
0

>>> pop (pop top) :: PosP BinP4
2

>>> pop (pop top) :: PosP BinP9
2

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

See top.

Showing

explicitShow :: PosP b -> String

explicitShow' :: PosP' n b -> String

explicitShowsPrec :: Int -> PosP b -> ShowS

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

Conversions

toNatural :: PosP b -> Natural

Convert PosP to Natural.

toNatural' :: forall n b. SNatI n => PosP' n b -> Natural

Convert PosP' to Natural.

Interesting

boring :: PosP BE

Counting to one is boring

>>> boring
0

Weakening (succ)

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

weakenRight1' :: forall b n. SBinP b -> PosP' n b -> PosP' n (Succ b)

Universe

universe :: forall b. SBinPI b => [PosP b]

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

universe' :: forall b n. (SNatI n, SBinPI b) => [PosP' n b]

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

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