Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Telescope
Synopsis
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 {
firstPart :: Telescope
secondPart :: Telescope
splitPerm :: Permutation
}
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 -> tSource
The permutation should permute the corresponding telescope. (left-to-right list)
renaming :: Permutation -> [Term]Source
If permute  : [a] -> [a], then substs (renaming ) : Term  -> Term 
renamingR :: Permutation -> [Term]Source
If permute  : [a] -> [a], then substs (renamingR ) : Term  -> Term 
flattenTel :: Telescope -> [Arg Type]Source
Flatten telescope: ( : Tel) -> [Type ]
reorderTel :: [Arg Type] -> PermutationSource
Order a flattened telescope in the correct dependeny order:  -> Permutation ( -> ~)
unflattenTel :: [String] -> [Arg Type] -> TelescopeSource
Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.
teleNames :: Telescope -> [String]Source
Get the suggested names from a telescope
teleArgNames :: Telescope -> [Arg String]Source
teleArgs :: Telescope -> ArgsSource
data SplitTel Source
A telescope split in two.
Constructors
SplitTel
firstPart :: Telescope
secondPart :: Telescope
splitPerm :: Permutation
splitTelescope :: Set Nat -> Telescope -> SplitTelSource
Split a telescope into the part that defines the given variables and the part that doesn't.
telView :: MonadTCM tcm => Type -> tcm TelViewSource
telViewUpTo :: MonadTCM tcm => Int -> Type -> tcm TelViewSource
telViewUpTo n t takes off the first n function types of t. Takes off all if $n < 0$.
piApplyM :: MonadTCM tcm => Type -> Args -> tcm TypeSource
A safe variant of piApply.
Produced by Haddock version 2.6.1