<br><div class="gmail_quote">On Thu, Oct 1, 2009 at 1:53 AM, Wolfgang Jeltsch <span dir="ltr"><<a href="mailto:g9ks157k@acme.softbase.org">g9ks157k@acme.softbase.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hello,<br><br>
> module Test where<br>
><br>
> open import Data.Unit<br>
><br>
> record R : Set₁ where<br>
><br>
> infixl 7 _*_<br>
> infixl 6 _+_<br>
><br>
> _+_ : Set → Set → Set<br>
> _+_ X Y = X<br>
><br>
> _*_ : Set → Set → Set<br>
> _*_ X Y = X<br>
><br>
> field<br>
> x : ⊤ + ⊤ * ⊤<br>
<br>
Agda tells me that it cannot parse the type ⊤ + ⊤ * ⊤. It seems as if the<br>
fixity declarations for _+_ and _*_ wouldn’t be taken into account. Is this a<br>
bug?<br>
<br>
Now I replace the line<br>
<br>
> _+_ X Y = X<br>
<br>
by<br>
<br>
> X + Y = X<br>
<br>
Now, Agda tells me that it cannot even parse the left-hand side X + Y, which<br>
surprises me. What surprises me even more is that Agda gives the Set₁ in the<br>
3rd non-empty line as the position of the error. Is this really correct? What<br>
have I missed?</blockquote><div><br></div><div>The problem is that the only definitions you're allowed before the fields in a record are definitions that could go in a let (at the moment, those are of the form f x y z = ...). The reason for this is that records are modelled by single constructor datatypes (with some eta rules) and so we need to be able to construct the type of this constructor. In your example the type would be</div>
<div><br></div><div><font class="Apple-style-span" face="'courier new', monospace"><span class="Apple-style-span" style="font-size: large;"> let _+_ : Set → Set → Set</span></font></div><font class="Apple-style-span" face="'courier new', monospace"><span class="Apple-style-span" style="font-size: large;"> _+_ X Y = X<br>
<br> _*_ : Set → Set → Set<br> _*_ X Y = X<br> in (x : ⊤ + ⊤ * ⊤) → R</span></font><div><br></div><div>Unfortunately you're not allowed fixity declarations in lets, which is why it doesn't parse. </div>
<div><br></div><div>/ Ulf</div></div>