Agda.TypeChecking.MetaVars.Occurs

Documentation

data OccursCtx

Constructors

Flex

Rigid

Instances

Eq OccursCtx

Show OccursCtx

abort :: OccursCtx -> TypeError -> TCM ()

class Occurs t where

Extended occurs check.

Methods

occurs :: OccursCtx -> MetaId -> [Nat] -> t -> TCM t

Instances

Occurs Sort

Occurs Type

Occurs Term

Occurs a => Occurs [a]

Occurs a => Occurs (Arg a)

Occurs a => Occurs (Abs a)

(Occurs a, Occurs b) => Occurs (a, b)

occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term

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 -> Bool

killArgs :: [Bool] -> MetaId -> TCM Bool

killedType :: [(Arg (String, Type), Bool)] -> Type -> ([Arg Bool], Type)

performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()