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

EqP PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

eqp :: forall (a :: k) (b :: k). PosP a -> PosP b -> Bool

GShow PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

gshowsPrec :: forall (a :: k). Int -> PosP a -> ShowS

OrdP PosP

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

comparep :: forall (a :: k) (b :: k). PosP a -> PosP b -> Ordering

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

SBinPI b => Function (PosP b)

Defined in Data.BinP.PosP

Methods

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

SBinPI b => Bounded (PosP b)

Defined in Data.BinP.PosP

Methods

minBound :: PosP b

maxBound :: PosP b

Show (PosP b)

Defined in Data.BinP.PosP

Methods

showsPrec :: Int -> PosP b -> ShowS

show :: PosP b -> String

showList :: [PosP b] -> ShowS

b ~ 'BE => Boring (PosP b)

Since: 0.1.2

Defined in Data.BinP.PosP

Methods

boring :: PosP b

NFData (PosP b)

Since: 0.1.2

Defined in Data.BinP.PosP

Methods

rnf :: 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

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 => GShow (PosP' n :: BinP -> Type)

Since: 0.1.3

Defined in Data.BinP.PosP

Methods

gshowsPrec :: forall (a :: k). Int -> PosP' n a -> ShowS

(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

(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) => Bounded (PosP' n b)

Defined in Data.BinP.PosP

Methods

minBound :: PosP' n b

maxBound :: 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

NFData (PosP' n b)

Since: 0.1.2

Defined in Data.BinP.PosP

Methods

rnf :: 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

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]