| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Modalities
Synopsis
- checkModality' :: QName -> Definition -> TCM (Maybe TypeError)
- checkModality :: QName -> Definition -> TCM ()
- checkModalityArgs :: Definition -> Args -> TCM ()
Documentation
checkModality' :: QName -> Definition -> TCM (Maybe TypeError) Source #
The second argument is the definition of the first.
checkModality :: QName -> Definition -> TCM () Source #
The second argument is the definition of the first.
checkModalityArgs :: Definition -> Args -> TCM () Source #
Checks that the given implicitely inserted arguments, are used in a modally correct way.