[Agda] Newbie Questions

[Ulf Norell]

Sorry for the late reply.

If I omit the implicit parameters,
>
>    revcat (x :: xs) ys = psuc (revcat xs (x :: ys))
>
> I would expect the computer to tell me that it needs more information to
> check the types.


If you use the emacs interface it does tell you. The location of the
unsolved implicit parameters will be highlighted and the types will be
displayed in the information buffer. If you're using the command line
version in interactive mode you have to ask for the information manually
using the command :meta.

II.
>
> Another question. I tried to repeat the example in Altenkirch,
> McBride, and McKinna's "Why Dependent Type Matters". The following
> datatype Tree intends to define a balanced tree:
>
>    data Tree (a : Set) : Nat -> Set where
>      Nul : Tree a zero
>      Tip : a -> Tree a (suc zero)
>      Bin : {m n : Nat} -> (p : Parity) ->
>            Tree a (parity p + n) -> Tree a n -> Tree a (parity p + (n
> + n))
>
> where parity : Parity -> Nat.
>
> Now, how do I match the size of a tree built with Bin? The following
> did not work:
>
>    insert : {a : Set} -> {n : Nat} ->
>                a -> Tree a n -> Tree a (suc n)
>    insert {a} {n} x (Bin Odd t u) = ...
>
> The computer complains that "parity p + (n' + n') != n of type Nat."
> Changing n to, for example p + (n + n), did not help..


When the value of an argument is determined by pattern matching on another
argument (in this case the value of n is determined to be parity Odd + (n +
n) by pattern matching on the tree) this has to be indicated by prefixing
the instantiated argument by a dot and writing the resulting instantiation
in place of the pattern. Writing out all the arguments in this example you
would get

insert {a} .{parity odd + (n + n)} x (Bin {m}{n} Odd t u) = ...

You don't have to write the implicit arguments explicitly, though, so you
can just say

insert x (Bin Odd t u) = ...

I hope this helps you. Don't hesitate to ask further questions if you run
into problems.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20070927/f99b6c1c/attachment.html