<div dir="ltr">On Mon, Nov 18, 2013 at 11:49 AM, Jan Stolarek <span dir="ltr"><<a href="mailto:jan.stolarek@p.lodz.pl" target="_blank">jan.stolarek@p.lodz.pl</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">[...]<br> = node l1 (merge r1 (node {i} l2 r2)))<br>
<br>
and I get an error in the last line for the innermost node constructor:<br>
<br>
Size !=< Set of type Set when checking that the expression i has type Set<br>
<br>
Why does it expect {i} to be Set? The definition of my data type is:<br>
<br>
data Tree (A : Set) : {i : Size} → Nat → Set where<br>
empty : {i : Size} → Tree A {↑ i} zero<br>
node : {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A {↑ i} (suc (l + r))<br>
<br></blockquote><div><br></div><div>When used in expressions, constructors take the parameters of their datatype as implicits so we get</div><div><br></div><div> node : {A : Set} {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A {↑ i} (suc (l + r))</div>
<div><br></div><div>so if you want to give "i" explicitly you have to use something like (node {i = i} l2 r2) instead.</div><div><br></div><div> </div><div>-- Andrea</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Janek<br>
<div class=""><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>