added Mutual

src/extra/Mutual.agda

@@ -0,0 +1,24 @@
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Bool using (Bool; true; false)
+
+data even : ℕ → Set
+data odd : ℕ → Set
+
+data even where
+  zero : even zero
+  suc : ∀ {n : ℕ} → odd n → even (suc n)
+data odd where
+  suc : ∀ {n : ℕ} → even n → odd (suc n)
+
+mutual
+  data even′ : ℕ → Set where
+    zero : even′ zero
+    suc : ∀ {n : ℕ} → odd′ n → even′ (suc n)
+  data odd′ : ℕ → Set where
+    suc : ∀ {n : ℕ} → even′ n → odd′ (suc n)
+
+{-
+/Users/wadler/sf/src/extra/Mutual.agda:3,6-10
+Missing definition for even
+-}
+