Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Telescope

Synopsis

Documentation

rename :: Subst t => Permutation -> t -> t

The permutation should permute the corresponding telescope. (left-to-right list)

renaming :: Permutation -> [Term]

If permute  : [a] -> [a], then substs (renaming ) : Term  -> Term 

renamingR :: Permutation -> [Term]

If permute  : [a] -> [a], then substs (renamingR ) : Term  -> Term 

flattenTel :: Telescope -> [Arg Type]

Flatten telescope: ( : Tel) -> [Type ]

reorderTel :: [Arg Type] -> Permutation

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

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

Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.

teleNames :: Telescope -> [String]

Get the suggested names from a telescope

data SplitTel

A telescope split in two.

splitTelescope :: Set Nat -> Telescope -> SplitTel

Split a telescope into the part that defines the given variables and the part that doesn't.

telView :: MonadTCM tcm => Type -> tcm TelView

telViewUpTo :: MonadTCM tcm => Int -> Type -> tcm TelView

telViewUpTo n t takes off the first n function types of t. Takes off all if $n < 0$.

piApplyM :: MonadTCM tcm => Type -> Args -> tcm Type

A safe variant of piApply.