Agda.Compiler.Treeless.Subst

Documentation

newtype UnderLambda

Constructors

UnderLambda Any

Instances

Eq UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: UnderLambda -> UnderLambda -> Bool

(/=) :: UnderLambda -> UnderLambda -> Bool

Ord UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: UnderLambda -> UnderLambda -> Ordering

(<) :: UnderLambda -> UnderLambda -> Bool

(<=) :: UnderLambda -> UnderLambda -> Bool

(>) :: UnderLambda -> UnderLambda -> Bool

(>=) :: UnderLambda -> UnderLambda -> Bool

max :: UnderLambda -> UnderLambda -> UnderLambda

min :: UnderLambda -> UnderLambda -> UnderLambda

Show UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> UnderLambda -> ShowS

show :: UnderLambda -> String

showList :: [UnderLambda] -> ShowS

Semigroup UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: UnderLambda -> UnderLambda -> UnderLambda

sconcat :: NonEmpty UnderLambda -> UnderLambda

stimes :: Integral b => b -> UnderLambda -> UnderLambda

Monoid UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: UnderLambda

mappend :: UnderLambda -> UnderLambda -> UnderLambda

mconcat :: [UnderLambda] -> UnderLambda

newtype SeqArg

Constructors

SeqArg All

Instances

Eq SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: SeqArg -> SeqArg -> Bool

(/=) :: SeqArg -> SeqArg -> Bool

Ord SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: SeqArg -> SeqArg -> Ordering

(<) :: SeqArg -> SeqArg -> Bool

(<=) :: SeqArg -> SeqArg -> Bool

(>) :: SeqArg -> SeqArg -> Bool

(>=) :: SeqArg -> SeqArg -> Bool

max :: SeqArg -> SeqArg -> SeqArg

min :: SeqArg -> SeqArg -> SeqArg

Show SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> SeqArg -> ShowS

show :: SeqArg -> String

showList :: [SeqArg] -> ShowS

Semigroup SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: SeqArg -> SeqArg -> SeqArg

sconcat :: NonEmpty SeqArg -> SeqArg

stimes :: Integral b => b -> SeqArg -> SeqArg

Monoid SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: SeqArg

mappend :: SeqArg -> SeqArg -> SeqArg

mconcat :: [SeqArg] -> SeqArg

data Occurs

Constructors

Occurs Int UnderLambda SeqArg

Instances

Eq Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: Occurs -> Occurs -> Bool

(/=) :: Occurs -> Occurs -> Bool

Ord Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: Occurs -> Occurs -> Ordering

(<) :: Occurs -> Occurs -> Bool

(<=) :: Occurs -> Occurs -> Bool

(>) :: Occurs -> Occurs -> Bool

(>=) :: Occurs -> Occurs -> Bool

max :: Occurs -> Occurs -> Occurs

min :: Occurs -> Occurs -> Occurs

Show Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> Occurs -> ShowS

show :: Occurs -> String

showList :: [Occurs] -> ShowS

Semigroup Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: Occurs -> Occurs -> Occurs

sconcat :: NonEmpty Occurs -> Occurs

stimes :: Integral b => b -> Occurs -> Occurs

Monoid Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: Occurs

mappend :: Occurs -> Occurs -> Occurs

mconcat :: [Occurs] -> Occurs

once :: Occurs

inSeq :: Occurs -> Occurs

underLambda :: Occurs -> Occurs

class HasFree a where

Minimal complete definition

freeVars

Methods

freeVars :: a -> Map Int Occurs

Instances

HasFree Int

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Int -> Map Int Occurs

HasFree TAlt

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs

HasFree TTerm

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs

HasFree a => HasFree [a]

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: [a] -> Map Int Occurs

HasFree a => HasFree (InSeq a)

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs

HasFree a => HasFree (Binder a)

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs

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

Defined in Agda.Compiler.Treeless.Subst

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)

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs

newtype InSeq a

Constructors

InSeq a

Instances

HasFree a => HasFree (InSeq a)

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs

tryStrengthen :: (HasFree a, Subst t a) => Int -> a -> Maybe a

Strenghtening.

Orphan instances

DeBruijn TTerm

Methods

deBruijnVar :: Int -> TTerm

debruijnNamedVar :: String -> Int -> TTerm

deBruijnView :: TTerm -> Maybe Int

Subst TTerm TAlt

Methods

applySubst :: Substitution' TTerm -> TAlt -> TAlt

Subst TTerm TTerm

Methods

applySubst :: Substitution' TTerm -> TTerm -> TTerm