Agda.TypeChecking.Substitute

Documentation

class Apply t where

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Methods

apply :: t -> Args -> t

Instances

Apply Permutation

Apply ClauseBody

Apply Clause

Apply Sort

Apply Type

Apply Term

Apply CompiledClauses

Apply FunctionInverse

Apply PrimFun

Apply Defn

Apply Definition

Apply DisplayTerm

Apply t => Apply [t]

Apply t => Apply (Maybe t)

Subst a => Apply (Tele a)

Apply t => Apply (Blocked t)

Apply a => Apply (Case a)

(Apply a, Apply b) => Apply (a, b)

Apply v => Apply (Map k v)

(Apply a, Apply b, Apply c) => Apply (a, b, c)

piApply :: Type -> Args -> Type

The type must contain the right number of pis without have to perform any reduction.

class Abstract t where

(abstract args v) args --> v[args].

Methods

abstract :: Telescope -> t -> t

Instances

Abstract Permutation

Abstract ClauseBody

Abstract Clause

Abstract Telescope

Abstract Sort

Abstract Type

Abstract Term

Abstract CompiledClauses

Abstract FunctionInverse

Abstract PrimFun

Abstract Defn

Abstract Definition

Abstract t => Abstract [t]

Abstract t => Abstract (Maybe t)

Abstract a => Abstract (Case a)

Abstract v => Abstract (Map k v)

telVars :: Functor f => Tele (f a) -> [f Pattern]

abstractArgs :: Abstract a => Args -> a -> a

type Substitution = [Term]

Substitutions.

class Subst t where

Substitute a term for the nth free variable.

Methods

substs :: Substitution -> t -> t

substUnder :: Nat -> Term -> t -> t

Instances

Subst Pattern

Subst ClauseBody

Subst LevelAtom

Subst PlusLevel

Subst Level

Subst Sort

Subst Type

Subst Term

Subst DisplayTerm

Subst Equality

Subst AsBinding

Subst DotPatternInst

Subst a => Subst [a]

Subst a => Subst (Maybe a)

Subst a => Subst (Arg a)

Subst a => Subst (Abs a)

Subst a => Subst (Tele a)

Subst t => Subst (Blocked t)

Subst a => Subst (HomHet a)

(Subst a, Subst b) => Subst (a, b)

idSub :: Telescope -> Substitution

subst :: Subst t => Term -> t -> t

class Raise t where

Add k to index of each open variable in x.

Methods

raiseFrom :: Nat -> Nat -> t -> t

renameFrom :: Nat -> (Nat -> Nat) -> t -> t

Instances

Raise ()

Raise Pattern

Raise ClauseBody

Raise LevelAtom

Raise PlusLevel

Raise Level

Raise Sort

Raise Elim

Raise Type

Raise Term

Raise DisplayTerm

Raise DisplayForm

Raise Constraint

Raise AsBinding

Raise t => Raise [t]

Raise t => Raise (Maybe t)

Raise t => Raise (Arg t)

Raise t => Raise (Abs t)

Raise a => Raise (Tele a)

Raise t => Raise (Blocked t)

Raise (Problem' p)

Raise a => Raise (HomHet a)

(Raise a, Raise b) => Raise (a, b)

Raise v => Raise (Map k v)

raise :: Raise t => Nat -> t -> t

rename :: Raise t => (Nat -> Nat) -> t -> t

data TelV a

Constructors

TelV (Tele (Arg a)) a

Instances

Functor TelV

Typeable1 TelV

(Eq a, Raise a) => Eq (TelV a)

Data a => Data (TelV a)

(Ord a, Raise a) => Ord (TelV a)

Show a => Show (TelV a)

type TelView = TelV Type

telFromList :: [Arg (String, Type)] -> Telescope

telToList :: Telescope -> [Arg (String, Type)]

telView' :: Type -> TelView

telePi :: Telescope -> Type -> Type

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

teleLam :: Telescope -> Term -> Term

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

absApp :: Subst t => Abs t -> Term -> t

Instantiate an abstraction

absBody :: Raise t => Abs t -> t

mkAbs :: (Raise a, Free a) => String -> a -> Abs a

reAbs :: (Raise a, Free a) => Abs a -> Abs a

sLub :: Sort -> Sort -> Sort

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term