[Agda] [agda2] how to programming the basic

[Sergei Meshveliani]

On Sun, 2016-01-24 at 12:52 +0000, Mandy Martino wrote:
> I use the script in tutorial and just append 2 
> 
> 
> Do it have priority of defining which first?
> 
> 
> Because +2 and *2  depend on each other
> 
> 
> I guess the original script in tutorial do not have this problem.


*2  uses  +2,  and +2 needs not to use *2.
Hence +2 needs to be defined earlier than *2.

If f uses g, and g uses f, then they need to be defined in the `mutual'
block:
  mutual 
    f : ...
    f = ... g ...

    g : ...
    g = ... f ...

Regards,

------
Sergei
 
> 
> 
> 
> 
>