- 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

# 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.

teleArgNames :: Telescope -> [Arg String]Source

A telescope split in two.