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

Agda.TypeChecking.MetaVars.Occurs

Synopsis

Documentation

class Occurs t whereSource

Extended occurs check.

Methods

occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM tSource

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 TermSource