Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.Treeless.Subst

Synopsis

Documentation

newtype SeqArg Source #

Constructors

SeqArg All 

Instances

Instances details
Monoid SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Semigroup SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Show SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

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

data Occurs Source #

Instances

Instances details
Monoid Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Semigroup Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Show Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

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

class HasFree a where Source #

Methods

freeVars :: a -> Map Int Occurs Source #

Instances

Instances details
HasFree TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

HasFree TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

HasFree Int Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

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

Defined in Agda.Compiler.Treeless.Subst

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

Defined in Agda.Compiler.Treeless.Subst

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

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: [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

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

Defined in Agda.Compiler.Treeless.Subst

newtype InSeq a Source #

Constructors

InSeq a 

Instances

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

Defined in Agda.Compiler.Treeless.Subst

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

Strenghtening.

Orphan instances

Subst TAlt Source # 
Instance details

Associated Types

type SubstArg TAlt Source #

Subst TTerm Source # 
Instance details

Associated Types

type SubstArg TTerm Source #

DeBruijn TTerm Source # 
Instance details