```
module Sets.Mutual where

open import Sets.Enumerated using (Bool; true; false)
open import Syntax.Decimal_Naturals using (ℕ; zero; suc)```

# Mutual definitions

In order to allow mutual definitions, one should declare any `Set` before using it. Those are called "forward declarations" — they are not unique to Agda.

Consider the following example for this:

```
-- forward declarations
data L : Set
data M : Set

-- actual declarations
data L where
nil : L
_∷_ : ℕ → M → L

data M where
_TT∷_ : Bool → L → M```

Note that `: Set` is missing from the definitions of the forward-declared sets.

## Exercises

1. What are the elements of `L` and `M`?

2. Define trees where each node can have arbitrary (finite) number of children (such as 0, 1, 2, and so on).

3. Define a language by the following grammar in Agda:

$E\to B$
$E\to I$
$I\to I+I$
$I\to I-I$
$I\to I*I$
$I\to z$
$I\to sI$
$B\to t$
$B\to f$
$B\to E=E$
$B\to E\ne E$

4. As a constant, give an element of the language defined in the previous exercise that contains the application of every rule at least once.