Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.MetaVars.Occurs
Synopsis
data OccursCtx
= Flex
| Rigid
abort :: OccursCtx -> TypeError -> TCM ()
class Occurs t where
occurs :: OccursCtx -> MetaId -> [Nat] -> t -> TCM t
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term
hasBadRigid :: [Nat] -> Term -> Bool
killArgs :: [Bool] -> MetaId -> TCM Bool
killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()
Documentation
data OccursCtx Source
Constructors
Flex
Rigid
abort :: OccursCtx -> TypeError -> TCM ()Source
class Occurs t whereSource
Extended occurs check.
Methods
occurs :: OccursCtx -> MetaId -> [Nat] -> t -> TCM tSource
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm TermSource
When assigning m xs := v, check that m does not occur in v and that the free variables of v are contained in xs.
hasBadRigid :: [Nat] -> Term -> BoolSource
killArgs :: [Bool] -> MetaId -> TCM BoolSource
killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)Source
performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()Source
Produced by Haddock version 2.6.1