| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Data.DeBruijn.Thinning.Fast
Synopsis
- data (n :: Nat) :<= (m :: Nat) where
- dropAll :: forall (m :: Nat). SNat m -> 'Z :<= m
- toBools :: forall (n :: Nat) (m :: Nat). (n :<= m) -> [Bool]
- fromTh :: forall bs (n :: Nat) (m :: Nat). Bits bs => (n :<= m) -> bs
- fromThRaw :: forall (n :: Nat) (m :: Nat). (n :<= m) -> ThRep
- data SomeTh = SomeTh {}
- fromBools :: Integral i => i -> [Bool] -> SomeTh
- toSomeTh :: (Integral i, Bits bs) => (i, bs) -> SomeTh
- toSomeThRaw :: (SNatRep, ThRep) -> SomeTh
- fromSomeTh :: (Integral i, Bits bs) => SomeTh -> (i, bs)
- fromSomeThRaw :: SomeTh -> (SNatRep, ThRep)
- class Thin (f :: Nat -> Type) where
- type ThRep = Natural
- bitsToThRep :: Bits bs => bs -> ThRep
- thRepToBits :: Bits bs => ThRep -> bs
- newtype (n :: Nat) :<= (m :: Nat) = UnsafeTh {}
Thinnings
data (n :: Nat) :<= (m :: Nat) where Source #
Bundled Patterns
| pattern KeepAll :: () => n ~ m => n :<= m | |
| pattern KeepOne :: () => (Pos n, Pos m) => (Pred n :<= Pred m) -> n :<= m | |
| pattern DropOne :: forall m n. () => Pos m => (n :<= Pred m) -> n :<= m |
toBools :: forall (n :: Nat) (m :: Nat). (n :<= m) -> [Bool] Source #
Convert a thinning into a list of booleans.
fromTh :: forall bs (n :: Nat) (m :: Nat). Bits bs => (n :<= m) -> bs Source #
Convert a thinning into a bit sequence.
Existential Wrapper
fromSomeTh :: (Integral i, Bits bs) => SomeTh -> (i, bs) Source #
Convert a thinning into a bit sequence.
The action of thinnings on Nat-indexed types
class Thin (f :: Nat -> Type) where Source #
The actions of thinnings on natural-indexed data types.
Methods
thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f n -> f m Source #
thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f m -> Maybe (f n) Source #
Fast
bitsToThRep :: Bits bs => bs -> ThRep Source #
thRepToBits :: Bits bs => ThRep -> bs Source #