gistfile1.txt

I've a similar issue with wanting to declare the fixity of a record parameter.
agda/agda#1787 (comment) points to this git issue, but how can this be applied to records?
Does

module _ {A : Set}  (_+_ : A → A → A) (let infixl 5 _+_; _+_ = _+_) where
  record Add : Set where
    field
      assoc : ∀ {m n o} → m + (n + o) ≡ m + n + o

have the same meaning and use as

record Add {A : Set} (p : A → A → A) : Set where
  infixl 5 _+_
  _+_ : A → A → A
  _+_ = p
  field
    assoc : ∀ {m n o} → m + (n + o) ≡ m + n + o

?
Can we use that module let syntax with records directly (without module) or are these two the only ways we have currently to declare a fixity for a record parameter?