- class Apply t where
- piApply :: Type -> Args -> Type
- class Abstract t where
- abstractArgs :: Abstract a => Args -> a -> a
- class Subst t where
- substs :: [Term] -> t -> t
- substUnder :: Nat -> Term -> t -> t
- idSub :: Telescope -> [Term]
- 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).
Apply Permutation | |
Apply ClauseBody | |
Apply Clause | |
Apply Telescope | |
Apply Sort | |
Apply Type | |
Apply Term | |
Apply FunctionInverse | |
Apply PrimFun | |
Apply Defn | |
Apply Definition | |
Apply DisplayTerm | |
Apply t => Apply [t] | |
Apply t => Apply (Maybe t) | |
Apply t => Apply (Blocked t) | |
(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 -> 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
Substitute a term for the nth free variable.
Subst Pattern | |
Subst ClauseBody | |
Subst Telescope | |
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) | |
(Data a, Subst a) => Subst (Abs a) | |
Subst t => Subst (Blocked t) | |
(Subst a, Subst b) => Subst (a, b) |
Add k
to index of each open variable in x
.