Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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

Documentation

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

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

renaming :: Permutation -> [Term] Source

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

renamingR :: Permutation -> [Term] Source

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

flattenTel :: Telescope -> [Arg Type] Source

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

reorderTel :: [Arg Type] -> Permutation Source

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

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

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

teleNames :: Telescope -> [String] Source

Get the suggested names from a telescope

teleArgNames :: Telescope -> [Arg String] Source

teleArgs :: Telescope -> Args Source

data SplitTel Source

A telescope split in two. Constructors SplitTel firstPart :: Telescope secondPart :: Telescope splitPerm :: Permutation

splitTelescope :: Set Nat -> Telescope -> SplitTel Source

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

Produced by Haddock version 2.6.0