HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Modulebin-0.1.4Haskell2010

Data.BinP.PosP

  • 2 types
  • 13 values
  • Packagebin-0.1.4
  • Exports15
  • LanguageHaskell2010
  • LicenceGPL-2.0-or-later
  • SourcePosP.hs
newtypenewtype PosP (b :: BinP)
#

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

Constructors

Instances12EqP, GShow, OrdP, Bounded, Eq, Ord, …
datadata PosP' (n :: Nat) (b :: BinP) where
#

PosP' is a structure inside PosP.

Constructors

Instances9GShow, Bounded, Eq, Ord, Show, NFData, …

Top & Pop

2 declarations
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

Showing

4 declarations

Conversions

2 declarations

Interesting

1 declaration
valueboring :: PosP 'BE
#

Counting to one is boring

Example1 expression
boring0

Weakening (succ)

2 declarations

Universe

2 declarations
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]