HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Fixity

Definitions for fixity, precedence levels, and declared syntax.

  • 4 types
  • 13 values
  • PackageAgda-2.7.0.1
  • Exports17
  • LanguageHaskell2010
  • LicenceMIT
  • SourceFixity.hs
datadata ThingWithFixity x
#

Decorating something with Fixity'.

Constructors

Instances8Functor, Foldable, Traversable, Show, Pretty, KillRange, …
datadata ParenPreference
#

Do we prefer parens around arguments like λ x → x or not? See lamBrackets.

PreferParenPreferParenless
Instances7Eq, Ord, Show, Generic, NFData, EmbPrj, …

Precendence

13 declarations
datadata Precedence
#

Precedence is associated with a context.

Constructors

Instances7Eq, Show, Generic, NFData, Pretty, EmbPrj, …
typetype PrecedenceStack = [Precedence]
#

When printing we keep track of a stack of precedences in order to be able to decide whether it's safe to leave out parens around lambdas. An empty stack is equivalent to TopCtx. Invariant: `notElem TopCtx`.

valuelamBrackets :: PrecedenceStack -> Bool
#

Does a lambda-like thing (lambda, let or pi) need brackets in the given context? A peculiar thing with lambdas is that they don't need brackets in certain right operand contexts. To decide we need to look at the stack of precedences and not just the current precedence. Example: m₁ >>= (λ x → x) >>= m₂ (for _>>=_ left associative).