From dc60739bd6232b5d82d594b418023d21d3bf84ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Sep 2020 09:22:18 -0700
Subject: [PATCH] feat: partition non recursive

---
 src/Lean/Elab/MutualDef.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 4df189521d..448a9815f0 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -667,6 +667,12 @@ compileDecl decl;
 applyAttributesOf preDecls AttributeApplicationTime.afterCompilation;
 pure ()
 
+private def partitionNonRec (preDecls : Array PreDeclaration) : Array PreDeclaration × Array PreDeclaration :=
+preDecls.partition fun predDecl =>
+  Option.isNone $ predDecl.value.find? fun c => match c with
+    | Expr.const declName _ _ => preDecls.any fun preDecl => preDecl.declName == declName
+    | _ => false
+
 def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
 scopeLevelNames ← getLevelNames;
 headers ← elabHeaders views;
@@ -686,6 +692,8 @@ withFunLocalDecls headers fun funFVars => do
       preDecls ← levelMVarToParamPreDecls preDecls;
       preDecls ← instantiateMVarsAtPreDecls preDecls;
       preDecls ← fixLevelParams preDecls scopeLevelNames allUserLevelNames;
+      let (preDeclsNonRec, preDecls) := partitionNonRec preDecls;
+      preDeclsNonRec.forM addAndCompileNonRec;
       -- TODO
       addAndCompileAsUnsafe preDecls