Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Fixity

Description

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

Synopsis

Documentation

data DoWarn Source #

Constructors

NoWarn 
DoWarn 

Instances

Instances details
Show DoWarn Source # 
Instance details

Defined in Agda.Syntax.Concrete.Fixity

Methods

showsPrec :: Int -> DoWarn -> ShowS

show :: DoWarn -> String

showList :: [DoWarn] -> ShowS

Eq DoWarn Source # 
Instance details

Defined in Agda.Syntax.Concrete.Fixity

Methods

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

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

fixitiesAndPolarities :: 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.