<br><br><div class="gmail_quote">On Tue, May 3, 2011 at 2:14 PM, Ondrej Rypacek <span dir="ltr"><<a href="mailto:ondrej.rypacek@gmail.com">ondrej.rypacek@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
Does anyone have an idea why can't I use k : src y == tgt x for (src<br>
(comp z y h) = tgt x) ?<br></blockquote><div><br></div><div>The checking of mutual blocks proceeds by first checking all the type signatures in the</div><div>block and then checking all the definitions (for datatypes, the constructors are considered</div>
<div>as the definition). This means that you are allowed to use a function in the type of a later</div><div>function, but it won't compute (since the definition hasn't been checked yet). In the definition</div><div>
of a function you can use any function in the mutual block, but only earlier functions will</div><div>compute. In the case of datatypes you can only use constructors of earlier datatypes in</div><div>a function definition.</div>
<div><br></div><div>In your example, since src is defined after tgt you can't use the knowledge that</div><div><meta charset="utf-8"><span class="Apple-style-span" style="border-collapse: collapse; font-family: arial, sans-serif; font-size: 13px; ">src (comp β α y) = src α in the definition of tgt. There are some ongoing work on allowing</span></div>
<div><span class="Apple-style-span" style="border-collapse: collapse; font-family: arial, sans-serif; font-size: 13px; ">more flexibility in the order things are checked in a mutual block, but for now you can work</span></div>
<div><span class="Apple-style-span" style="border-collapse: collapse; font-family: arial, sans-serif; font-size: 13px; ">around the issue by postponing the checking of the problematic clause:</span></div><div><span class="Apple-style-span" style="border-collapse: collapse; font-family: arial, sans-serif; font-size: 13px; "><br>
</span></div><div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> mutual</span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> data W : Set where</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> comp : (β α : W) → src β ≡ tgt α → W</span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> alpha : (z y x : W) → src z ≡ tgt y → src y ≡ tgt x → W</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"><br></span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> tgt : W → W</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> tgt (comp β α y) = tgt β</span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> tgt (alpha z y x h k) = tgt-alpha z y x h k</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"><br></span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> src : W → W</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> src (comp β α y) = src α</span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> src (alpha z y x h k) = comp z (comp y x k) h</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"><br></span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> tgt-alpha : ∀ z y x h k → W</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"> tgt-alpha z y x h k = comp (comp z y h) x k</span></font></div></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"><br>
</span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;">Since tgt-alpha is defined after src we can use the definition of src and the problem goes away.</span></font></div>
<div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;"><br></span></font></div><div><font class="Apple-style-span" face="arial, sans-serif"><span class="Apple-style-span" style="border-collapse: collapse;">/ Ulf</span></font></div>
</div>