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 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 |
Orphan instances
Subst TAlt Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source # | |||||
Subst TTerm Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm Source # | |||||
DeBruijn TTerm Source # | |||||