Agda.Syntax.Concrete.Fixity

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

Documentation

type Fixities = Map Name Fixity'

type Polarities = Map Name [Occurrence]

class Monad m => MonadFixityError m where

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> m a

throwMultiplePolarityPragmas :: [Name] -> m a

warnUnknownNamesInFixityDecl :: HasCallStack => [Name] -> m ()

warnUnknownNamesInPolarityPragmas :: HasCallStack => [Name] -> m ()

warnUnknownFixityInMixfixDecl :: HasCallStack => [Name] -> m ()

warnPolarityPragmasButNotPostulates :: HasCallStack => [Name] -> m ()

Instances

MonadFixityError ScopeM

Defined in Agda.Syntax.Scope.Monad

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> ScopeM a

throwMultiplePolarityPragmas :: [Name] -> ScopeM a

warnUnknownNamesInFixityDecl :: [Name] -> ScopeM ()

warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM ()

warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM ()

warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM ()

data DoWarn

Constructors

NoWarn

DoWarn

Instances

Show DoWarn

Defined in Agda.Syntax.Concrete.Fixity

Methods

showsPrec :: Int -> DoWarn -> ShowS

show :: DoWarn -> String

showList :: [DoWarn] -> ShowS

Eq DoWarn

Defined in Agda.Syntax.Concrete.Fixity

Methods

(==) :: DoWarn -> DoWarn -> Bool

(/=) :: DoWarn -> DoWarn -> Bool

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

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.