[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