Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Modalities

Synopsis

Documentation

checkModality' :: MonadConversion m => QName -> Definition -> m (Maybe TypeError) Source #

The second argument is the definition of the first.

checkModality :: MonadConversion m => QName -> Definition -> m () Source #

The second argument is the definition of the first.

checkModalityArgs :: MonadConversion m => Definition -> Args -> m () Source #

Checks that the given implicitely inserted arguments, are used in a modally correct way.