[Agda] order inside a mutual block is relevant?

[Andreas Abel]

A mutual block is checked by first checking the type signatures, in  
order, and then the definitions, in order.

To check   x : t   you need  t : Set,  and to check  x = true  you  
need to unfold  t = Bool.

Agda does not reorder the definitions for you.  It might be difficult  
in the presence of hidden arguments.


On Sep 25, 2010, at 5:23 PM, David Leduc wrote:

> I was expecting that the order of definitions inside a mutual block
> was irrelevant.
> The definition below is accepted by the type checker.
> But if I change the order of definitions of x and t, then it is  
> rejected.
> Isn't it odd?
>
> module test where
>
> open import Data.Bool
>
> mutual
>
>  t : Set
>  t = Bool
>
>  x : t
>  x = true
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/