[Agda] mutual recursion

[Ulf Norell]

On Tue, May 3, 2011 at 2:14 PM, Ondrej Rypacek <ondrej.rypacek at gmail.com>wrote:

>
> Does anyone have an idea why can't I use k : src y == tgt x for (src
> (comp z y h) = tgt x) ?
>

The checking of mutual blocks proceeds by first checking all the type
signatures in the
block and then checking all the definitions (for datatypes, the constructors
are considered
as the definition). This means that you are allowed to use a function in the
type of a later
function, but it won't compute (since the definition hasn't been checked
yet). In the definition
of a function you can use any function in the mutual block, but only earlier
functions will
compute. In the case of datatypes you can only use constructors of earlier
datatypes in
a function definition.

In your example, since src is defined after tgt you can't use the knowledge
that
src (comp β α y) = src α in the definition of tgt. There are some ongoing
work on allowing
more flexibility in the order things are checked in a mutual block, but for
now you can work
around the issue by postponing the checking of the problematic clause:

 mutual
   data W : Set where
     comp : (β α : W) → src β ≡ tgt α → W
     alpha : (z y x : W) → src z ≡ tgt y → src y ≡ tgt x → W

   tgt : W → W
   tgt (comp β α y) = tgt β
   tgt (alpha z y x h k) = tgt-alpha z y x h k

   src : W → W
   src (comp β α y) = src α
   src (alpha z y x h k) = comp z (comp y x k) h

   tgt-alpha : ∀ z y x h k → W
   tgt-alpha z y x h k = comp (comp z y h) x k

Since tgt-alpha is defined after src we can use the definition of src and
the problem goes away.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110503/6d0f954f/attachment.html