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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Modalities

Synopsis

- checkModality' :: MonadConversion m => QName -> Definition -> m (Maybe TypeError)
- checkModality :: MonadConversion m => QName -> Definition -> m ()
- checkModalityArgs :: MonadConversion m => Definition -> Args -> m ()

# 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.