Agda.TypeChecking.Modalities

valuecheckModality'

The second argument is the definition of the first.

valuecheckModality :: MonadConversion m => QName -> Definition -> m ()

The second argument is the definition of the first.

valuecheckModalityArgs :: MonadConversion m => Definition -> Args -> m ()

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