Add test

tests/lean/invalidMutualError.lean

@@ -0,0 +1,17 @@
+/-! Test invalid mutual block error message -/
+
+inductive Foo : Type where
+  | foo0 : Nat → Foo
+  | foo1 : Foo → Foo
+  | foo2 : Foo → Foo → Foo
+
+mutual
+
+  inductive Bar1 : Foo → Prop where
+    | mk {f : Foo} : Bar f → Bar1 (.foo1 f)
+
+  def Bar : Foo → Prop
+    | .foo1 f => Bar1 f
+    | _ => True
+
+end

tests/lean/invalidMutualError.lean.expected.out

@@ -0,0 +1 @@
+invalidMutualError.lean:8:0: error: invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs