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.