Safe Haskell  None 

Language  Haskell98 
 data OutputTypeName
 getOutputTypeName :: Type > TCM OutputTypeName
 renameP :: Subst t a => Permutation > a > a
 renaming :: forall a. DeBruijn a => Permutation > Substitution' a
 renamingR :: DeBruijn a => Permutation > Substitution' a
 flattenTel :: Telescope > [Dom Type]
 reorderTel :: [Dom Type] > Maybe Permutation
 reorderTel_ :: [Dom Type] > Permutation
 unflattenTel :: [ArgName] > [Dom Type] > Telescope
 teleNames :: Telescope > [ArgName]
 teleArgNames :: Telescope > [Arg ArgName]
 teleArgs :: DeBruijn a => Telescope > [Arg a]
 teleNamedArgs :: DeBruijn a => Telescope > [NamedArg a]
 permuteTel :: Permutation > Telescope > Telescope
 varDependencies :: Telescope > IntSet > IntSet
 data SplitTel = SplitTel {}
 splitTelescope :: VarSet > Telescope > SplitTel
 splitTelescopeExact :: [Int] > Telescope > Maybe SplitTel
 instantiateTelescope :: Telescope > Int > Term > Maybe (Telescope, PatternSubstitution, Permutation)
 expandTelescopeVar :: Telescope > Int > Telescope > ConHead > (Telescope, PatternSubstitution)
 telView :: Type > TCM TelView
 telViewUpTo :: Int > Type > TCM TelView
 telViewUpTo' :: Int > (Dom Type > Bool) > Type > TCM TelView
 mustBePi :: MonadTCM tcm => Type > tcm (Dom Type, Abs Type)
 ifPi :: MonadTCM tcm => Term > (Dom Type > Abs Type > tcm a) > (Term > tcm a) > tcm a
 ifPiType :: MonadTCM tcm => Type > (Dom Type > Abs Type > tcm a) > (Type > tcm a) > tcm a
 ifNotPi :: MonadTCM tcm => Term > (Term > tcm a) > (Dom Type > Abs Type > tcm a) > tcm a
 ifNotPiType :: MonadTCM tcm => Type > (Type > tcm a) > (Dom Type > Abs Type > tcm a) > tcm a
 piApplyM :: Type > Args > TCM Type
 piApply1 :: MonadTCM tcm => Type > Term > tcm Type
 intro1 :: MonadTCM tcm => Type > (Type > tcm a) > tcm a
 addTypedInstance :: QName > Type > TCM ()
 resolveUnknownInstanceDefs :: TCM ()
 getInstanceDefs :: TCM InstanceTable
Documentation
data OutputTypeName Source #
getOutputTypeName :: Type > TCM OutputTypeName Source #
Strips all Pi's and return the head definition name, if possible.
renameP :: Subst t a => Permutation > a > a Source #
The permutation should permute the corresponding telescope. (lefttoright list)
renaming :: forall a. DeBruijn a => Permutation > Substitution' a Source #
If permute π : [a]Γ > [a]Δ
, then applySubst (renaming π) : Term Γ > Term Δ
renamingR :: DeBruijn a => Permutation > Substitution' a Source #
If permute π : [a]Γ > [a]Δ
, then applySubst (renamingR π) : Term Δ > Term Γ
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 normalise
d.
reorderTel_ :: [Dom Type] > Permutation Source #
unflattenTel :: [ArgName] > [Dom Type] > Telescope Source #
Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.
permuteTel :: Permutation > Telescope > Telescope Source #
Permute telescope: permutes or drops the types in the telescope according to the given permutation. Assumes that the permutation preserves the dependencies in the telescope.
varDependencies :: Telescope > IntSet > IntSet Source #
Recursively computes dependencies of a set of variables in a given telescope. Any dependencies outside of the telescope are ignored.
A telescope split in two.
SplitTel  

:: VarSet  A set of de Bruijn indices. 
> Telescope  Original telescope. 
> SplitTel 

Split a telescope into the part that defines the given variables and the part that doesn't.
See prop_splitTelescope
.
:: [Int]  A list of de Bruijn indices 
> Telescope  The telescope to split 
> Maybe SplitTel 

As splitTelescope, but fails if any additional variables or reordering would be needed to make the first part welltyped.
:: Telescope  ⊢ Γ 
> Int  Γ ⊢ var k : A 
> Term  Γ ⊢ u : A 
> Maybe (Telescope, PatternSubstitution, Permutation) 
Try to instantiate one variable in the telescope (given by its de Bruijn level) with the given value, returning the new telescope and a substitution to the old one. Returns Nothing if the given value depends (directly or indirectly) on the variable.
expandTelescopeVar :: Telescope > Int > Telescope > ConHead > (Telescope, PatternSubstitution) Source #
Try to etaexpand one variable in the telescope (given by its de Bruijn level)
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
.
ifPi :: MonadTCM tcm => Term > (Dom Type > Abs Type > tcm a) > (Term > tcm a) > tcm a Source #
If the given type is a Pi
, pass its parts to the first continuation.
If not (or blocked), pass the reduced type to the second continuation.
ifPiType :: MonadTCM tcm => Type > (Dom Type > Abs Type > tcm a) > (Type > tcm a) > tcm a Source #
If the given type is a Pi
, pass its parts to the first continuation.
If not (or blocked), pass the reduced type to the second continuation.
ifNotPi :: MonadTCM tcm => Term > (Term > tcm a) > (Dom Type > Abs Type > tcm a) > tcm a Source #
If the given type is blocked or not a Pi
, pass it reduced to the first continuation.
If it is a Pi
, pass its parts to the second continuation.
ifNotPiType :: MonadTCM tcm => Type > (Type > tcm a) > (Dom Type > Abs Type > tcm a) > tcm a Source #
If the given type is blocked or not a Pi
, pass it reduced to the first continuation.
If it is a Pi
, pass its parts to the second continuation.
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
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.