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