Agda-2.2.6: 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
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.
Produced by Haddock version 2.4.2