[Agda] How to set up fixities for record parameters?

Vag Vagoff vag.vagoff at gmail.com
Thu Jul 8 12:07:11 CEST 2010


module Groups where

infix 8 _≡_  ; data _≡_ {A : Set} (a : A) : A → Set where ·≡· : a ≡ a -- just for testing

Op : Set → Set {- An operation on A -}
Op A = A → A → A

record MonoidOn (A : Set) (_+_ _×_ : Op A)  (e : A) : Set where
     infixl 40 _+_
     infixl 50 _×_
     field
         move : ∀ {X Y a} → X + Y × a ≡ X × a + Y
         last : ∀ {X a} → X + a ≡ X × a
         left-unit : ∀ {X} → e + X ≡ X
         right-unit : ∀ {X} → X + e ≡ X

How to set up fixities for _+_ and _×_?
Compiler complains at any position I've tried.

Thanks in advance,
sincerely yours,
Vag.


More information about the Agda mailing list