Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Telescope

Contents

Instance definitions

Synopsis

Documentation

data OutputTypeName Source

Constructors

OutputTypeName QName
OutputTypeNameNotYetKnown
NoOutputTypeName

getOutputTypeName :: Type -> TCM OutputTypeName Source

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

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

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

renaming :: Permutation -> Substitution Source

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

renamingR :: Permutation -> Substitution Source

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

flattenTel :: Telescope -> [Dom Type] Source

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

reorderTel :: [Dom Type] -> Maybe Permutation Source

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

Since reorderTel tel uses free variable analysis of type in tel, the telescope should be normalised.

reorderTel_ :: [Dom Type] -> Permutation Source

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

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

teleNames :: Telescope -> [ArgName] Source

Get the suggested names from a telescope

teleArgNames :: Telescope -> [Arg ArgName] Source

teleArgs :: Telescope -> Args Source

data SplitTel Source

A telescope split in two.

Constructors

SplitTel
Fields firstPart :: Telescope secondPart :: Telescope splitPerm :: Permutation The permutation takes us from the original telescope to `firstPart ++ secondPart`.

splitTelescope Source

Arguments

:: VarSet	A set of de Bruijn indices.
-> Telescope	Original telescope.
-> SplitTel	`firstPart` mentions the given variables, `secondPart` not.

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

See prop_splitTelescope.

telView :: Type -> TCM TelView Source

telViewUpTo :: Int -> Type -> TCM TelView Source

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 Source

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

mustBePi :: MonadTCM tcm => Type -> tcm (Dom Type, Abs Type) Source

Decomposing a function type.

piApplyM :: Type -> Args -> TCM Type Source

A safe variant of piApply.

piApply1 :: MonadTCM tcm => Type -> Term -> tcm Type Source

intro1 :: MonadTCM tcm => Type -> (Type -> tcm a) -> tcm a Source

Given a function type, introduce its domain into the context and continue with its codomain.

Instance definitions

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

resolveUnknownInstanceDefs :: TCM () Source

getInstanceDefs :: TCM InstanceTable Source

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.