[Agda] Help with proofs

[Nils Anders Danielsson]

On Sun, May 4, 2008 at 5:10 PM, Tristan Wibberley <tristan at wibberley.org> wrote:
>
>  [...] This is in preference from
>  allowing the proof objects to be the same sometimes and not others
>  because the rule for when it is allowed and when it isn't is difficult
>  to grok.

If the rule is difficult to grok, then maybe we have not explained it
properly:

* A function can only be applied to an argument if the type of the
  argument is equivalent to that expected by the function.
* Two types are equivalent iff they have the same normal form.

To understand when two terms have the same normal form you need to
know how functions defined using pattern matching are evaluated. Since
Agda has to handle open terms the rules may be a bit more complicated
than you are used to. See

  http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.PatternMatching

-- 
/NAD