[Agda] Induction-induction in a tricky order

[Dr. ERDI Gergo]

On Tue, 15 Mar 2016, Dr. ERDI Gergo wrote:

> If you put them in a 'mutual' block, that should be OK (as long as positivity 
> blah blah blah).

Sorry, by this I meant you should put your 'normal' definitions (without 
the 'forward' `data` declarations) in a `mutual` block:

mutual
   data Foo : Set where MkFoo : Bar -> Foo
   data Bar : Set where MkBar : Foo -> Bar

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Why experiment on animals when there are so many lawyers?