[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