| Safe Haskell | Safe-Inferred |
|---|---|
| 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.