Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.MetaVars.Occurs
Synopsis
class Occurs t where
occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM t
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term
Documentation
class Occurs t whereSource
Extended occurs check.
Methods
occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM tSource
show/hide Instances
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm TermSource
Produced by Haddock version 2.4.2