Agda-2.5.1: A dependently typed functional programming language and proof assistant
Agda.Compiler.Treeless.Subst
newtype UnderLambda Source
Constructors
Instances
newtype SeqArg Source
data Occurs Source
once :: Occurs Source
inSeq :: Occurs -> Occurs Source
underLambda :: Occurs -> Occurs Source
class HasFree a where Source
Methods
freeVars :: a -> 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