Safe Haskell	None
Language	GHC2021

Data.DeBruijn.Environment

Contents

Synopsis

data Env (n :: Nat) a where
- pattern Nil :: () => n ~ 'Z => Env n a
- pattern (:>) :: () => Pos n => Env (Pred n) a -> a -> Env n a
(!) :: forall (n :: Nat) a. Env n a -> Ix n -> a

Environments

data Env (n :: Nat) a where #

Bundled Patterns

pattern Nil :: () => n ~ 'Z => Env n a
pattern (:>) :: () => Pos n => Env (Pred n) a -> a -> Env n a

Instances details

Foldable (Env n)
Instance details Defined in Data.DeBruijn.Environment.Fast Methods fold :: Monoid m => Env n m -> m # foldMap :: Monoid m => (a -> m) -> Env n a -> m # foldMap' :: Monoid m => (a -> m) -> Env n a -> m # foldr :: (a -> b -> b) -> b -> Env n a -> b # foldr' :: (a -> b -> b) -> b -> Env n a -> b # foldl :: (b -> a -> b) -> b -> Env n a -> b # foldl' :: (b -> a -> b) -> b -> Env n a -> b # foldr1 :: (a -> a -> a) -> Env n a -> a # foldl1 :: (a -> a -> a) -> Env n a -> a # toList :: Env n a -> [a] # null :: Env n a -> Bool # length :: Env n a -> Int # elem :: Eq a => a -> Env n a -> Bool # maximum :: Ord a => Env n a -> a # minimum :: Ord a => Env n a -> a # sum :: Num a => Env n a -> a # product :: Num a => Env n a -> a #
Traversable (Env n)
Instance details Defined in Data.DeBruijn.Environment.Fast Methods traverse :: Applicative f => (a -> f b) -> Env n a -> f (Env n b) # sequenceA :: Applicative f => Env n (f a) -> f (Env n a) # mapM :: Monad m => (a -> m b) -> Env n a -> m (Env n b) # sequence :: Monad m => Env n (m a) -> m (Env n a) #
Functor (Env n)
Instance details Defined in Data.DeBruijn.Environment.Fast Methods fmap :: (a -> b) -> Env n a -> Env n b # (<$) :: a -> Env n b -> Env n a #

(!) :: forall (n :: Nat) a. Env n a -> Ix n -> a #