| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.Treeless.Subst
Contents
Synopsis
- newtype UnderLambda = UnderLambda Any
- newtype SeqArg = SeqArg All
- data Occurs = Occurs Int UnderLambda SeqArg
- once :: Occurs
- inSeq :: Occurs -> Occurs
- underLambda :: Occurs -> Occurs
- class HasFree a where
- freeIn :: HasFree a => Int -> a -> Bool
- occursIn :: HasFree a => Int -> a -> Occurs
- data Binder a = Binder Int a
- newtype InSeq a = InSeq a
- tryStrengthen :: (HasFree a, Subst t a) => Int -> a -> Maybe a
Documentation
newtype UnderLambda Source #
Constructors
| UnderLambda Any |
Instances
Constructors
| Occurs Int UnderLambda SeqArg |
underLambda :: Occurs -> Occurs Source #
Constructors
| InSeq a |