Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Treeless.Subst

Contents

Documentation

newtype SeqArg #

Constructors

SeqArg All 

class HasFree a where #

Minimal complete definition

freeVars

Methods

freeVars :: a -> Map Int Occurs #

Instances

HasFree Int # 

Methods

freeVars :: Int -> Map Int Occurs #

HasFree TAlt # 

Methods

freeVars :: TAlt -> Map Int Occurs #

HasFree TTerm # 

Methods

freeVars :: TTerm -> Map Int Occurs #

HasFree a => HasFree [a] # 

Methods

freeVars :: [a] -> Map Int Occurs #

HasFree a => HasFree (InSeq a) # 

Methods

freeVars :: InSeq a -> Map Int Occurs #

HasFree a => HasFree (Binder a) # 

Methods

freeVars :: Binder a -> Map Int Occurs #

(HasFree a, HasFree b) => HasFree (a, b) # 

Methods

freeVars :: (a, b) -> Map Int Occurs #

freeIn :: HasFree a => Int -> a -> Bool #

occursIn :: HasFree a => Int -> a -> Occurs #

data Binder a #

Constructors

Binder Int a 

Instances

HasFree a => HasFree (Binder a) # 

Methods

freeVars :: Binder a -> Map Int Occurs #

newtype InSeq a #

Constructors

InSeq a 

Instances

HasFree a => HasFree (InSeq a) # 

Methods

freeVars :: InSeq a -> Map Int Occurs #

Orphan instances