bin-0.1.1: Bin: binary natural numbers.
Safe HaskellSafe
LanguageHaskell2010

Data.BinP.PosP

Synopsis

Documentation

newtype PosP (b :: BinP) Source #

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

Constructors

PosP 

Fields

Instances

Instances details
SBinPI b => Bounded (PosP b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

minBound :: PosP b #

maxBound :: PosP b #

Eq (PosP b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

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

Ord (PosP b) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

showsPrec :: Int -> PosP b -> ShowS #

show :: PosP b -> String #

showList :: [PosP b] -> ShowS #

SBinPI b => Function (PosP b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

SBinPI b => Arbitrary (PosP b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

arbitrary :: Gen (PosP b) #

shrink :: PosP b -> [PosP b] #

CoArbitrary (PosP b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

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

PosP' is a structure inside PosP.

Constructors

AtEnd 

Fields

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

    position is either at the last digit;

Here 

Fields

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

Instances details
(SNatI n, SBinPI b) => Bounded (PosP' n b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

minBound :: PosP' n b #

maxBound :: PosP' n b #

Eq (PosP' n b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

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

Ord (PosP' n b) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

(SNatI n, SBinPI b) => Arbitrary (PosP' n b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

arbitrary :: Gen (PosP' n b) #

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

SNatI n => CoArbitrary (PosP' n b) Source # 
Instance details

Defined in Data.BinP.PosP

Methods

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

Top & Pop

top :: SBinPI b => PosP b Source #

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 Source #

See top.

Showing

Conversions

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

Convert PosP' to Natural.

Interesting

boring :: PosP 'BE Source #

Counting to one is boring

>>> boring
0

Weakening (succ)

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

Universe

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

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

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

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

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