Safe Haskell	None
Language	GHC2021

Data.DeBruijn.Thinning

Contents

Synopsis

data (n :: Nat) :<= (m :: Nat) where
- 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
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 {
- lower :: SNat n
- upper :: SNat m
- value :: n :<= m
}
fromBools :: Integral i => i -> [Bool] -> SomeTh
toSomeTh :: (Integral i, Bits bs) => (i, bs) -> SomeTh
toSomeThRaw :: (SNatRep, ThRep) -> SomeTh
class Thin (f :: Nat -> Type) where
- thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f n -> f m
- thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f m -> Maybe (f n)
type ThRep = Natural

Thinnings

data (n :: Nat) :<= (m :: Nat) where #

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

Instances details

Thin ((:<=) l)
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= n) -> l :<= m # thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= m) -> Maybe (l :<= n) #
Show (n :<= m)
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods showsPrec :: Int -> (n :<= m) -> ShowS # show :: (n :<= m) -> String # showList :: [n :<= m] -> ShowS #
NFData (n :<= m)
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods rnf :: (n :<= m) -> () #
Eq (n :<= m)
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods (==) :: (n :<= m) -> (n :<= m) -> Bool # (/=) :: (n :<= m) -> (n :<= m) -> Bool #

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 #

Existential Wrapper

Constructors

SomeTh
Fields lower :: SNat n upper :: SNat m value :: n :<= m

Instances details

Show SomeTh
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods showsPrec :: Int -> SomeTh -> ShowS # show :: SomeTh -> String # showList :: [SomeTh] -> ShowS #
NFData SomeTh
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods rnf :: SomeTh -> () #
Eq SomeTh
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods (==) :: SomeTh -> SomeTh -> Bool # (/=) :: SomeTh -> SomeTh -> Bool #

toSomeTh :: (Integral i, Bits bs) => (i, bs) -> SomeTh #

class Thin (f :: Nat -> Type) where #

Methods

thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f n -> f m #

thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> f m -> Maybe (f n) #

Instances details

Thin Ix
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m # thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n) #
Thin ((:<=) l)
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= n) -> l :<= m # thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= m) -> Maybe (l :<= n) #