ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Concrete.Fixity

Collecting fixity declarations (and polarity pragmas) for concrete declarations.

Synopsis

type Fixities
type Polarities
class MonadFixityError
data DoWarn
value fixitiesAndPolarities

PackageAgda-2.8.0.2
Exports5
LanguageHaskell2010
LicenceMIT
SourceFixity.hs

typetype Fixities = Map Name Fixity'

typetype Polarities = Map Name PragmaPolarities

classclass Monad m => MonadFixityError (m :: Type -> Type) where

Methods

throwMultipleFixityDecls :: List1 (Name, Pair Fixity') -> m a
throwMultiplePolarityPragmas :: List1 Name -> m a
warnUnknownNamesInFixityDecl :: HasCallStack => Set1 Name -> m ()
warnUnknownNamesInPolarityPragmas :: HasCallStack => Set1 Name -> m ()
warnUnknownFixityInMixfixDecl :: HasCallStack => Set1 Name -> m ()
warnPolarityPragmasButNotPostulates :: HasCallStack => Set1 Name -> m ()
warnEmptyPolarityPragma :: HasCallStack => Range -> m ()

Instances1MonadFixityError

MonadFixityError ScopeMDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Monad · orphan

datadata DoWarn

NoWarn DoWarn

Instances2Eq, Show

Eq DoWarnDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Fixity
Show DoWarnDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Fixity

valuefixitiesAndPolarities

:: MonadFixityError m
=> DoWarn
-> [Declaration]
-> m (Fixities, Polarities)

Source#

Get the fixities and polarity pragmas from the current block. Doesn't go inside modules and where blocks. The reason for this is that these declarations have to appear at the same level (or possibly outside an abstract or mutual block) as their target declaration.