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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Treeless.Subst

Contents

Synopsis

Documentation

newtype UnderLambda Source #

Constructors

UnderLambda Any 
Instances
Eq UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Show UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> UnderLambda -> ShowS

show :: UnderLambda -> String

showList :: [UnderLambda] -> ShowS

Semigroup UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty UnderLambda -> UnderLambda

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

Monoid UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

newtype SeqArg Source #

Constructors

SeqArg All 
Instances
Eq SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord SeqArg Source # 
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 Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> SeqArg -> ShowS

show :: SeqArg -> String

showList :: [SeqArg] -> ShowS

Semigroup SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty SeqArg -> SeqArg

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

Monoid SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

data Occurs Source #

Constructors

Occurs Int UnderLambda SeqArg 
Instances
Eq Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Ord Occurs Source # 
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 Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> Occurs -> ShowS

show :: Occurs -> String

showList :: [Occurs] -> ShowS

Semigroup Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty Occurs -> Occurs

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

Monoid Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

class HasFree a where Source #

Methods

freeVars :: a -> Map Int Occurs Source #

Instances
HasFree Int Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Int -> Map Int Occurs Source #

HasFree TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs Source #

HasFree TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs Source #

HasFree a => HasFree [a] Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs Source #

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

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs Source #

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

Defined in Agda.Compiler.Treeless.Subst

Methods

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

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

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

data Binder a Source #

Constructors

Binder Int a 
Instances
HasFree a => HasFree (Binder a) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs Source #

newtype InSeq a Source #

Constructors

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

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs Source #

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

Strenghtening.

Orphan instances

DeBruijn TTerm Source # 
Instance details

Methods

deBruijnVar :: Int -> TTerm Source #

debruijnNamedVar :: String -> Int -> TTerm Source #

deBruijnView :: TTerm -> Maybe Int Source #

Subst TTerm TAlt Source # 
Instance details

Subst TTerm TTerm Source # 
Instance details