Support mutual data declarations

[ratmice]

I was "for science'ing" mutual inductive QPF things, Attempting to declare a mutually recursive uninhabited type similar to Void below.

What I noticed is that when using the mutual keyword, with the data parser, only the first thing ends up being exported into the namespace.

This is visible below if you uncomment the #check attempt1.Hell or the #print prefix output.

import data.fix.parser.equations
namespace Void
    data Void
    | void : Void → Void
    -- Should complain about synthesizing type 
    -- if you try to #eval the following:
    #check Void.void (Void.void _)
end Void

/- What about mutually inductive variations of Void?
   Here we have something almost works -/
namespace attempt1
    mutual data Snowball, Hell
    with Snowball : Type
    | snowball : Snowball → Snowball
    with Hell : Π α : Type, Type
    | hell : Snowball → Hell Snowball

    #check attempt1.Snowball
    #check attempt1.Snowball.snowball 
    -- Only the first part of any mutual seems to appear.
    --#check attempt1.Hell
    -- #print prefix attempt1
end attempt1

/- This is i guess more like what i was after,
   I could not figure out a way to get it through the type checker
   without introducing a new inhabited type 'Thing' -/
namespace attempt2
    mutual data Thing, Snowball, Hell
    with Thing : Type
    | is : Thing
    with Snowball : Π α : Type, Type
    | snowball : Hell Thing → Snowball Thing
    with Hell : Π α : Type, Type
    | hell : Snowball Thing  → Hell Thing

    #check (Thing.is)
    -- #print prefix attempt2
end attempt2

[digama0]

Mutual definitions are planned but not yet supported.