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

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
- telView :: MonadTCM tcm => Type -> tcm TelView
- telViewUpTo :: MonadTCM tcm => Int -> Type -> tcm TelView
- piApplyM :: MonadTCM tcm => Type -> Args -> tcm Type

# 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

teleArgNames :: Telescope -> [Arg String]

teleArgs :: Telescope -> Args

data SplitTel

A telescope split in two.

Constructors

SplitTel |

Fields

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

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.