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

Agda.TypeChecking.MetaVars.Occurs

Synopsis

Documentation

data OccursCtx

Constructors

Flex 
Rigid 

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.

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