Agda.TypeChecking.Substitute
- class Apply t where
- piApply :: Type -> Args -> Type
- class Abstract t where
- abstractArgs :: Abstract a => Args -> a -> a
- type Substitution = [Term]
- class Subst t where
- substs :: Substitution -> t -> t
- substUnder :: Nat -> Term -> t -> t
- idSub :: Telescope -> Substitution
- subst :: Subst t => Term -> t -> t
- absApp :: Subst t => Abs t -> Term -> t
- class Raise t where
- raise :: Raise t => Nat -> t -> t
- data TelView = TelV Telescope Type
- telView' :: Type -> TelView
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- dLub :: Sort -> Abs Sort -> Sort
Documentation
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
piApply :: Type -> Args -> TypeSource
The type must contain the right number of pis without have to perform any reduction.
(abstract args v) args --> v[args].
abstractArgs :: Abstract a => Args -> a -> aSource
type Substitution = [Term]Source
Substitutions.
Substitute a term for the nth free variable.
idSub :: Telescope -> SubstitutionSource
Add k to index of each open variable in x.