[Agda] Termination problems with "with" and recursion

[Andrea Vezzosi]

On Mon, Nov 18, 2013 at 11:49 AM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:

> [...]
>           = node l1 (merge r1 (node {i} l2 r2)))
>
> and I get an error in the last line for the innermost node constructor:
>
>   Size !=< Set of type Set when checking that the expression i has type Set
>
> Why does it expect {i} to be Set? The definition of my data type is:
>
> data Tree (A : Set) : {i : Size} → Nat → Set where
>   empty : {i : Size} → Tree A {↑ i} zero
>   node  : {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A
> {↑ i} (suc (l + r))
>
>
When used in expressions, constructors take the parameters of their
datatype as implicits so we get

  node : {A : Set} {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r →
Tree A {↑ i} (suc (l + r))

so if you want to give "i" explicitly you have to use something like (node
{i = i} l2 r2) instead.


-- Andrea


> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131118/9eb3dd98/attachment.html