Agda-2.5.1.1: A dependently typed functional programming language and proof assistant
Agda.Compiler.Treeless.Subst
Contents
newtype UnderLambda Source #
Constructors
Instances
Methods
(==) :: UnderLambda -> UnderLambda -> Bool #
(/=) :: UnderLambda -> UnderLambda -> Bool #
compare :: UnderLambda -> UnderLambda -> Ordering #
(<) :: UnderLambda -> UnderLambda -> Bool #
(<=) :: UnderLambda -> UnderLambda -> Bool #
(>) :: UnderLambda -> UnderLambda -> Bool #
(>=) :: UnderLambda -> UnderLambda -> Bool #
max :: UnderLambda -> UnderLambda -> UnderLambda #
min :: UnderLambda -> UnderLambda -> UnderLambda #
showsPrec :: Int -> UnderLambda -> ShowS #
show :: UnderLambda -> String #
showList :: [UnderLambda] -> ShowS #
mempty :: UnderLambda #
mappend :: UnderLambda -> UnderLambda -> UnderLambda #
mconcat :: [UnderLambda] -> UnderLambda #
newtype SeqArg Source #
(==) :: SeqArg -> SeqArg -> Bool #
(/=) :: SeqArg -> SeqArg -> Bool #
compare :: SeqArg -> SeqArg -> Ordering #
(<) :: SeqArg -> SeqArg -> Bool #
(<=) :: SeqArg -> SeqArg -> Bool #
(>) :: SeqArg -> SeqArg -> Bool #
(>=) :: SeqArg -> SeqArg -> Bool #
max :: SeqArg -> SeqArg -> SeqArg #
min :: SeqArg -> SeqArg -> SeqArg #
showsPrec :: Int -> SeqArg -> ShowS #
show :: SeqArg -> String #
showList :: [SeqArg] -> ShowS #
mempty :: SeqArg #
mappend :: SeqArg -> SeqArg -> SeqArg #
mconcat :: [SeqArg] -> SeqArg #
data Occurs Source #
(==) :: Occurs -> Occurs -> Bool #
(/=) :: Occurs -> Occurs -> Bool #
compare :: Occurs -> Occurs -> Ordering #
(<) :: Occurs -> Occurs -> Bool #
(<=) :: Occurs -> Occurs -> Bool #
(>) :: Occurs -> Occurs -> Bool #
(>=) :: Occurs -> Occurs -> Bool #
max :: Occurs -> Occurs -> Occurs #
min :: Occurs -> Occurs -> Occurs #
showsPrec :: Int -> Occurs -> ShowS #
show :: Occurs -> String #
showList :: [Occurs] -> ShowS #
mempty :: Occurs #
mappend :: Occurs -> Occurs -> Occurs #
mconcat :: [Occurs] -> Occurs #
once :: Occurs Source #
inSeq :: Occurs -> Occurs Source #
underLambda :: Occurs -> Occurs Source #
class HasFree a where Source #
Minimal complete definition
freeVars
freeVars :: a -> Map Int Occurs Source #
freeVars :: Int -> Map Int Occurs Source #
freeVars :: TAlt -> Map Int Occurs Source #
freeVars :: TTerm -> Map Int Occurs Source #
freeVars :: [a] -> Map Int Occurs Source #
freeVars :: InSeq a -> Map Int Occurs Source #
freeVars :: Binder a -> Map Int Occurs Source #
freeVars :: (a, b) -> Map Int Occurs Source #
freeIn :: HasFree a => Int -> a -> Bool Source #
occursIn :: HasFree a => Int -> a -> Occurs Source #
data Binder a Source #
newtype InSeq a Source #
debruijnVar :: Int -> TTerm Source #
debruijnNamedVar :: String -> Int -> TTerm Source #
debruijnView :: TTerm -> Maybe Int Source #
applySubst :: Substitution' TTerm -> TAlt -> TAlt Source #
applySubst :: Substitution' TTerm -> TTerm -> TTerm Source #