- data OccursCtx
- abort :: OccursCtx -> TypeError -> TCM ()
- class Occurs t where
- 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 ()