[Agda] Importing Infix Operation Inside a Record From Record Field (Indentation fixed)

[Nils Anders Danielsson]

On 2009-10-27 19:30, Vag Vagoff wrote:
> Why associativity does not work for ⊛ in `composition' field?

Apparently fixity declarations are ignored for let-bound variables. I
have reported this bug:

  http://code.google.com/p/agda/issues/detail?id=213

> How to fix this record to do its job and leave readability high?

The following code works:

  record IsApplicative (t : Set → Set) : Set₁ where
    field
      applicative : Applicative t

    open Applicative applicative

    field
      composition : ∀ {a b c} {u : t (b → a)} {v : t (c → b)} {w : t c} →
                    pure _◦_ ⊛ u ⊛ v ⊛ w ≡ u ⊛ (v ⊛ w)

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.