feat: check kinds

src/Lean/Elab/MutualDef.lean

@@ -34,6 +34,13 @@ unless (m₁.isPartial == m₂.isPartial) $
   throwError "cannot mix partial and non-partial definitions";
 pure ()
 
+def checkKinds (k₁ k₂ : DefKind) : TermElabM Unit := do
+unless (k₁.isExample == k₂.isExample) $
+  throwError "cannot mix examples and definitions"; -- Reason: we should discard examples
+unless (k₁.isTheorem == k₂.isTheorem) $
+  throwError "cannot mix theorems and definitions"; -- Reason: we will eventually elaborate theorems in `Task`s.
+pure ()
+
 def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) :=
 views.foldlM
   (fun (headers : Array DefViewElabHeader) (view : DefView) => withRef view.ref do
@@ -60,6 +67,7 @@ views.foldlM
             unless (levelNames == firstHeader.levelNames) $
               throwError "universe parameters mismatch in mutual definition";
             checkModifiers view.modifiers firstHeader.modifiers;
+            checkKinds view.kind firstHeader.kind;
             forallTelescopeCompatible type firstHeader.type xs.size fun _ _ _ => pure ())
           (fun ex => match ex with
             | Exception.error ref msg => throw (Exception.error ref ("invalid mutually recursive definitions, " ++ msg))

tests/lean/mutualdef1.lean

@@ -61,3 +61,27 @@ def g (x : Nat) : Nat → Nat -- universe parameter mistmatch
 | x+1 => f x
 
 end
+
+
+mutual
+
+def f (x : Nat) : Nat → Nat
+| 0   => 1
+| x+1 => g x
+
+theorem g (x : Nat) : Nat → Nat -- cannot mix theorems and definitions
+| 0   => 2
+| x+1 => f x
+
+end
+
+mutual
+
+def f  : Nat → Nat
+| 0   => 1
+| x+1 => g x
+
+example : Nat := -- cannot mix examples and definitions
+g 10
+
+end

tests/lean/mutualdef1.lean.expected.out

@@ -6,3 +6,5 @@ mutualdef1.lean:22:0: error: invalid mutually recursive definitions, parameter n
 mutualdef1.lean:35:0: error: invalid mutually recursive definitions, binder annotation mismatch at parameter 'x'
 mutualdef1.lean:47:0: error: invalid mutually recursive definitions, number of parameters mismatch
 mutualdef1.lean:59:0: error: invalid mutually recursive definitions, universe parameters mismatch in mutual definition
+mutualdef1.lean:72:0: error: invalid mutually recursive definitions, cannot mix theorems and definitions
+mutualdef1.lean:84:0: error: invalid mutually recursive definitions, cannot mix examples and definitions