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

Vag vag.vagoff at gmail.com
Thu Jul 8 17:51:43 CEST 2010


And the same for modules:

module G (A : Set) (_×_ : Op A) (g : A) (_+_ : Op A)  (e : A) where
     infixl 40 _+_
     infixl 50 _×_
     postulate move : ∀ {X Y a} → X + Y × a ≡ X × a + Y
     postulate last : ∀ {X a} → X + a ≡ X × a

How to set fixities for + and ×?

This not works also:

record Concatenative' (A : Set) (cross : Op A) (g : A) (plus : Op A)  (e : A) : Set where
     _+_ = plus
     _×_ = cross
     infixl 40 _+_
     infixl 50 _×_
     field
         move : ∀ {X Y a} → X + Y × a ≡ X × a + Y
         last : ∀ {X a} → X + a ≡ X × a

But this works ok:

module Grp' (A : Set) (cross : Op A) (g : A) (plus : Op A)  (e : A) where
     _+_ = plus
     _×_ = cross
     infixl 40 _+_
     infixl 50 _×_
     postulate
         move : ∀ {X Y a} → X + Y × a ≡ X × a + Y
         last : ∀ {X a} → X + a ≡ X × a


Thanks in advance,
Vag.


More information about the Agda mailing list