Agda.TypeChecking.Telescope

Documentation

data OutputTypeName

Constructors

OutputTypeName QName

OutputTypeNameNotYetKnown

NoOutputTypeName

getOutputTypeName :: Type -> TCM OutputTypeName

Strips all Pi's and return the head definition name, if possible.

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

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

renaming :: Permutation -> Substitution

renamingR :: Permutation -> Substitution

flattenTel :: Telescope -> [Dom Type]

Flatten telescope: (

reorderTel :: [Dom Type] -> Maybe Permutation

Order a flattened telescope in the correct dependeny order:

reorderTel_ :: [Dom Type] -> Permutation

unflattenTel :: [ArgName] -> [Dom Type] -> Telescope

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

teleNames :: Telescope -> [ArgName]

Get the suggested names from a telescope

teleArgNames :: Telescope -> [Arg ArgName]

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.

Instance definitions

addTypedInstance :: QName -> Type -> TCM ()

resolveUnknownInstanceDefs :: TCM ()

getInstanceDefs :: TCM InstanceTable

Try to solve the instance definitions whose type is not yet known, report an error if it doesn't work and return the instance table otherwise.