Agda.TypeChecking.Telescope
- rename :: Subst t => Permutation -> t -> t
- renaming :: Permutation -> [Term]
- renamingR :: Permutation -> [Term]
- flattenTel :: Telescope -> [Arg Type]
- reorderTel :: [Arg Type] -> Permutation
- unflattenTel :: [String] -> [Arg Type] -> Telescope
- teleNames :: Telescope -> [String]
- teleArgNames :: Telescope -> [Arg String]
- teleArgs :: Telescope -> Args
- data SplitTel = SplitTel {}
- splitTelescope :: Set Nat -> Telescope -> SplitTel
- telView :: MonadTCM tcm => Type -> tcm TelView
- telViewUpTo :: MonadTCM tcm => Int -> Type -> tcm TelView
- piApplyM :: MonadTCM tcm => Type -> Args -> tcm Type
Documentation
rename :: Subst t => Permutation -> t -> t
The permutation should permute the corresponding telescope. (left-to-right list)
renaming :: Permutation -> [Term]
If permute : [a] -> [a]
, then substs (renaming ) : Term -> Term
renamingR :: Permutation -> [Term]
If permute : [a] -> [a]
, then substs (renamingR ) : Term -> Term
flattenTel :: Telescope -> [Arg Type]
Flatten telescope: ( : Tel) -> [Type ]
reorderTel :: [Arg Type] -> Permutation
Order a flattened telescope in the correct dependeny order: -> Permutation ( -> ~)
unflattenTel :: [String] -> [Arg Type] -> Telescope
Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.
teleArgNames :: Telescope -> [Arg String]
splitTelescope :: Set Nat -> Telescope -> SplitTel
Split a telescope into the part that defines the given variables and the part that doesn't.
telViewUpTo :: MonadTCM tcm => Int -> Type -> tcm TelView
telViewUpTo n t
takes off the first n
function types of t
.
Takes off all if $n < 0$.