Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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

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

renaming :: Permutation -> SubstitutionSource

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

renamingR :: Permutation -> SubstitutionSource

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

flattenTel :: Telescope -> [Dom Type]Source

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

reorderTel :: [Dom Type] -> Maybe PermutationSource

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

unflattenTel :: [String] -> [Dom Type] -> TelescopeSource

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

teleNames :: Telescope -> [String]Source

Get the suggested names from a telescope

data SplitTel Source

A telescope split in two.

splitTelescope :: VarSet -> Telescope -> SplitTelSource

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

telViewUpTo :: Int -> Type -> TCM TelViewSource

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 TelViewSource

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 TypeSource

A safe variant of piApply.