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

Safe Haskell | None

Agda.TypeChecking.Telescope

Synopsis

- renameP :: Subst t => Permutation -> t -> t
- renaming :: Permutation -> Substitution
- renamingR :: Permutation -> Substitution
- flattenTel :: Telescope -> [Dom Type]
- reorderTel :: [Dom Type] -> Maybe Permutation
- reorderTel_ :: [Dom Type] -> Permutation
- unflattenTel :: [String] -> [Dom Type] -> Telescope
- teleNames :: Telescope -> [String]
- teleArgNames :: Telescope -> [Arg String]
- teleArgs :: Telescope -> Args
- data SplitTel = SplitTel {
  - firstPart :: Telescope
  - secondPart :: Telescope
  - splitPerm :: Permutation
  }
- splitTelescope :: VarSet -> Telescope -> SplitTel
- telView :: Type -> TCM TelView
- telViewUpTo :: Int -> Type -> TCM TelView
- telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView
- piApplyM :: Type -> Args -> TCM Type

# Documentation

renameP :: Subst t => Permutation -> t -> t

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

renaming :: Permutation -> Substitution

If `permute π : [a]Γ -> [a]Δ`, then `applySubst (renaming π) : Term Γ -> Term Δ`

renamingR :: Permutation -> Substitution

If `permute π : [a]Γ -> [a]Δ`, then `substs (renamingR π) : Term Δ -> Term Γ`

flattenTel :: Telescope -> [Dom Type]

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

reorderTel :: [Dom Type] -> Maybe Permutation

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

reorderTel_ :: [Dom Type] -> Permutation

unflattenTel :: [String] -> [Dom 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 :: VarSet -> Telescope -> SplitTel

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

telView :: Type -> TCM TelView

telViewUpTo :: Int -> Type -> TCM TelView

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

telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView

`telViewUpTo' n p t` takes off $t$ the first `n` (or arbitrary many if `n < 0`) function domains as long as they satify `p`.

piApplyM :: Type -> Args -> TCM Type

A safe variant of piApply.