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

Safe Haskell	None
Language	Haskell98

Agda.Compiler.Treeless.Subst

Documentation

newtype UnderLambda Source

Constructors

UnderLambda Any

Instances

Eq UnderLambda Source
Ord UnderLambda Source
Show UnderLambda Source
Monoid UnderLambda Source

newtype SeqArg Source

Constructors

Instances

Eq SeqArg Source
Ord SeqArg Source
Show SeqArg Source
Monoid SeqArg Source

data Occurs Source

Constructors

Occurs Int UnderLambda SeqArg

Instances

Eq Occurs Source
Ord Occurs Source
Show Occurs Source
Monoid 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

Instances

HasFree Int Source
HasFree TAlt Source
HasFree TTerm Source
HasFree a => HasFree [a] Source
HasFree a => HasFree (InSeq a) Source
HasFree a => HasFree (Binder a) Source
(HasFree a, HasFree b) => HasFree (a, b) Source

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

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

data Binder a Source

Constructors

Instances

HasFree a => HasFree (Binder a) Source

newtype InSeq a Source

Constructors

Instances

HasFree a => HasFree (InSeq a) Source