| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 -> t | Source

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] -> Permutation | Source

Order a flattened telescope in the correct dependeny order: -> Permutation ( -> ~)

unflattenTel :: [String] -> [Arg Type] -> Telescope | Source

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 -> Args | Source

data SplitTel | Source

A telescope split in two.
Constructors

SplitTel |

firstPart :: Telescope |
secondPart :: Telescope |
splitPerm :: Permutation |

splitTelescope :: Set Nat -> Telescope -> SplitTel | Source

Split a telescope into the part that defines the given variables and the part that doesn't.
Produced by Haddock version 2.4.2