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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Treeless.Subst

Contents

Synopsis

Documentation

newtype UnderLambda #

Constructors

UnderLambda Any 
Instances
Eq UnderLambda # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord UnderLambda # 
Instance details

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 # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> UnderLambda -> ShowS #

show :: UnderLambda -> String #

showList :: [UnderLambda] -> ShowS #

Semigroup UnderLambda # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty UnderLambda -> UnderLambda #

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

Monoid UnderLambda # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: UnderLambda #

mappend :: UnderLambda -> UnderLambda -> UnderLambda #

mconcat :: [UnderLambda] -> UnderLambda #

newtype SeqArg #

Constructors

SeqArg All 
Instances
Eq SeqArg # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord SeqArg # 
Instance details

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 # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> SeqArg -> ShowS #

show :: SeqArg -> String #

showList :: [SeqArg] -> ShowS #

Semigroup SeqArg # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty SeqArg -> SeqArg #

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

Monoid SeqArg # 
Instance details

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 # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord Occurs # 
Instance details

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 # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> Occurs -> ShowS #

show :: Occurs -> String #

showList :: [Occurs] -> ShowS #

Semigroup Occurs # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty Occurs -> Occurs #

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

Monoid Occurs # 
Instance details

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 # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Int -> Map Int Occurs #

HasFree TAlt # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs #

HasFree TTerm # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs #

HasFree a => HasFree [a] # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

HasFree a => HasFree (InSeq a) # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs #

HasFree a => HasFree (Binder a) # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs #

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

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) # 
Instance details

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) # 
Instance details

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 # 
Instance details

Methods

deBruijnVar :: Int -> TTerm #

debruijnNamedVar :: String -> Int -> TTerm #

deBruijnView :: TTerm -> Maybe Int #

Subst TTerm TAlt # 
Instance details

Methods

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

Subst TTerm TTerm # 
Instance details

Methods

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