Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.MetaVars.Occurs

Synopsis

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 Term Source

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 Source

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

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

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