[Agda] Induction-induction in a tricky order

[Jesper Cockx]

The following seems to work:

data Foo : Set
> data Bar : Foo → Set
> data Bar2 : Foo → Set
>
> bar2-temp : (x : Foo) → Bar2 x
>
> data Foo where
>   foo   : (x : Foo) → Bar x → Bar2 x → Foo
>
> data Bar where
>   bar   : (x : Foo) → Bar x
>   bar'  : (x : Foo) → Bar (foo x (bar x) (bar2-temp x))
>
> data Bar2 where
>   bar2  : (x : Foo) → Bar2 x
>   bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))
>
> bar2-temp = bar2
>

It seems a little silly that constructors cannot be references before they
are defined, even when inside a mutual block. There also seems to be a
difference between the old- and new-style mutual blocks when referencing
datatypes. Maybe we could improve Agda to handle situations like this more
uniformly?

cheers,
Jesper


On Tue, Mar 15, 2016 at 4:03 PM, Simon Boulier <simon.boulier at ens-rennes.fr>
wrote:

>
> This way?
>
> mutual
>   data Foo : Set where
>     foo   : (x : Foo) → Bar x → Bar2 x → Foo
>
>   data Bar : Foo → Set where
>     bar   : (x : Foo) → Bar x
>     bar'  : (x : Foo) → Bar (foo x (bar x) (bar2 x))
>
>   data Bar2 : Foo → Set where
>     bar2  : (x : Foo) → Bar2 x
>     bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))
>
> I doesn't seem to change anything for me...
> Agda still complains that bar2 is not in scope when type checking bar'.
>
>
>
>
> Le 15/03/2016 15:50, Dr. ERDI Gergo a écrit :
>
> On Tue, 15 Mar 2016, Simon Boulier wrote:
>
> Is it a way to type check the following:
>       data Foo  : Set
>       data Bar  : Foo → Set
>       data Bar2 : Foo → Set
>
>       data Foo where
>         foo   : (x : Foo) → Bar x → Bar2 x → Foo
>
> ...
>
> If you put them in a 'mutual' block, that should be OK (as long as
> positivity blah blah blah).
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160315/f9aa2fb1/attachment-0001.html