Fixity

Content created by Fredrik Bakke and Fernando Chu.

Created on 2023-04-27.
Last modified on 2023-09-10.

module reflection.fixity where
Imports 
open import elementary-number-theory.addition-integers

open import foundation.identity-types
open import foundation.universe-levels

open import primitives.floats

open import reflection.names

Idea

The fixity of a quoted name is given by

  • An associativity, i.e. it is left-associative, right-associative or neither.
  • A precedence, i.e. it is unrelated (it has no precedence) or it is related and has a float precedence.

Definition

data Associativity : UU lzero where
  left-associative : Associativity
  right-associative : Associativity
  non-associative : Associativity

data Precedence : UU lzero where
  related : Float → Precedence
  unrelated : Precedence

data Fixity : UU lzero where
  fixity : Associativity → Precedence → Fixity

{-# BUILTIN ASSOC Associativity #-}
{-# BUILTIN ASSOCLEFT left-associative #-}
{-# BUILTIN ASSOCRIGHT right-associative #-}
{-# BUILTIN ASSOCNON non-associative #-}

{-# BUILTIN PRECEDENCE Precedence #-}
{-# BUILTIN PRECRELATED related #-}
{-# BUILTIN PRECUNRELATED unrelated #-}

{-# BUILTIN FIXITY Fixity #-}
{-# BUILTIN FIXITYFIXITY fixity #-}

primitive
  primQNameFixity : Name → Fixity

Examples

_ : primQNameFixity (quote add-ℤ) ＝ fixity non-associative unrelated
_ = refl

_ : primQNameFixity (quote (_+ℤ_)) ＝ fixity left-associative (related 35.0)
_ = refl

Recent changes