[Agda] Re: Simple DepType Pattern Matching

[Ulf Norell]

On Sun, Sep 13, 2009 at 5:40 PM, Yuya Uezato <ranha at ymail.com> wrote:

> Hi Wouter.
>
> But,there are things that has not understood yet.
>
> 1.Why must use a indirect method?
> <<code>>
> f : (Th unit) -> Unit
> f (th unit) = unit
> <<code>>
> It seems to be correct...
>
> u != unit of type Unit
> when checking that the pattern th unit has type Th unit
>

The error message here is not very good. Basically what's happening is that
the type checker is doing the case splitting step by step and type checking
each of the steps. The first step in this case is (for some variable u)

f (th u) = ...

which you've already observed is not correct. If you use the "make case"
command (C-c C-c) in the emacs mode you'd get f (th .unit) right away.

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