Safe Haskell	None
Language	GHC2021

Data.DeBruijn.Index

Contents

Synopsis

data Ix (n :: Nat) where
- pattern FZ :: () => Pos n => Ix n
- pattern FS :: () => Pos n => Ix (Pred n) -> Ix n
eqIx :: forall (n :: Nat) (m :: Nat). Ix n -> Ix m -> Bool
fromIx :: forall i (n :: Nat). Integral i => Ix n -> i
fromIxRaw :: forall (n :: Nat). Ix n -> IxRep
isPos :: forall (n :: Nat) a. Ix n -> (Pos n => a) -> a
thin :: forall (n :: Nat). Ix ('S n) -> Ix n -> Ix ('S n)
thick :: forall (n :: Nat). Ix ('S n) -> Ix ('S n) -> Maybe (Ix n)
inject :: forall (n :: Nat) (m :: Nat). Ix n -> SNat m -> Ix (n + m)
raise :: forall (n :: Nat) (m :: Nat). SNat n -> Ix m -> Ix (n + m)
data SomeIx = SomeIx {
- bound :: !(SNat n)
- index :: !(Ix n)
}
withSomeIx :: (forall (n :: Nat). SNat n -> Ix n -> a) -> SomeIx -> a
toSomeIx :: (Integral n, Integral i) => (n, i) -> SomeIx
toSomeIxRaw :: (SNatRep, IxRep) -> SomeIx
fromSomeIx :: (Integral n, Integral i) => SomeIx -> (n, i)
fromSomeIxRaw :: SomeIx -> (SNatRep, IxRep)
type IxRep = Int

DeBruijn Indexes

data Ix (n :: Nat) where #

Bundled Patterns

pattern FZ :: () => Pos n => Ix n
pattern FS :: () => Pos n => Ix (Pred n) -> Ix 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) #
Show (Ix n)
Instance details Defined in Data.DeBruijn.Index.Fast Methods showsPrec :: Int -> Ix n -> ShowS # show :: Ix n -> String # showList :: [Ix n] -> ShowS #
NFData (Ix n)
Instance details Defined in Data.DeBruijn.Index.Fast Methods rnf :: Ix n -> () #
Eq (Ix n)
Instance details Defined in Data.DeBruijn.Index.Fast Methods (==) :: Ix n -> Ix n -> Bool # (/=) :: Ix n -> Ix n -> Bool #

eqIx :: forall (n :: Nat) (m :: Nat). Ix n -> Ix m -> Bool #

fromIx :: forall i (n :: Nat). Integral i => Ix n -> i #

fromIxRaw :: forall (n :: Nat). Ix n -> IxRep #

isPos :: forall (n :: Nat) a. Ix n -> (Pos n => a) -> a #

thin :: forall (n :: Nat). Ix ('S n) -> Ix n -> Ix ('S n) #

thick :: forall (n :: Nat). Ix ('S n) -> Ix ('S n) -> Maybe (Ix n) #

inject :: forall (n :: Nat) (m :: Nat). Ix n -> SNat m -> Ix (n + m) #

raise :: forall (n :: Nat) (m :: Nat). SNat n -> Ix m -> Ix (n + m) #

Existential Wrapper

Constructors

SomeIx
Fields bound :: !(SNat n) index :: !(Ix n)

Instances details

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

withSomeIx :: (forall (n :: Nat). SNat n -> Ix n -> a) -> SomeIx -> a #