|
Agda.TypeChecking.Telescope |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
The permutation should permute the corresponding telescope. (left-to-right list)
|
|
|
If permute : [a] -> [a], then substs (renaming ) : Term -> Term
|
|
|
If permute : [a] -> [a], then substs (renamingR ) : Term -> Term
|
|
|
Flatten telescope: ( : Tel) -> [Type ]
|
|
|
Order a flattened telescope in the correct dependeny order: ->
Permutation ( -> ~)
|
|
|
Unflatten: turns a flattened telescope into a proper telescope. Must be
properly ordered.
|
|
|
Get the suggested names from a telescope
|
|
|
|
|
|
|
A telescope split in two.
| Constructors | |
|
|
|
Split a telescope into the part that defines the given variables and the
part that doesn't.
|
|
|
|
|
telViewUpTo n t takes off the first n function types of t.
Takes off all if $n < 0$.
|
|
|
A safe variant of piApply.
|
|
Produced by Haddock version 2.6.1 |