max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: partition non recursive

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-05 09:22:18 -07:00
parent 3ae3c51a8c
commit dc60739bd6
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/MutualDef.lean
View file

@ -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