Agda-2.2.6: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.MetaVars.Occurs
Synopsis
class Occurs t whereSource
Extended occurs check.
Methods
occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM tSource
Instances
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm TermSource