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

feat: add addAndCompileAsUnsafe

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-05 07:56:02 -07:00
parent 9b788db91f
commit 91cedab090
1 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -626,6 +626,24 @@ pure $ preDecls.map fun preDecl =>
val := fixExpr preDecl.val,
lparams := lparams }
private def applyAttributesOf (preDecls : Array PreDeclaration) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
preDecls.forM fun preDecl => applyAttributes preDecl.declName preDecl.modifiers.attrs applicationTime
private def addAndCompileAsUnsafe (preDecls : Array PreDeclaration) : TermElabM Unit := do
let decl := Declaration.mutualDefnDecl $ preDecls.toList.map fun preDecl => {
name := preDecl.declName,
lparams := preDecl.lparams,
type := preDecl.type,
value := preDecl.val,
isUnsafe := true,
hints := ReducibilityHints.opaque
};
addDecl decl;
applyAttributesOf preDecls AttributeApplicationTime.afterTypeChecking;
compileDecl decl;
applyAttributesOf preDecls AttributeApplicationTime.afterCompilation;
pure ()
def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
scopeLevelNames ← getLevelNames;
headers ← elabHeaders views;
@ -646,8 +664,7 @@ withFunLocalDecls headers fun funFVars => do
preDecls ← instantiateMVarsAtPreDecls preDecls;
preDecls ← fixLevelParams preDecls scopeLevelNames allUserLevelNames;
-- TODO
preDecls.forM fun preDecl => IO.println (toString preDecl.declName ++ " : " ++ toString preDecl.type ++ " :=\n" ++ toString preDecl.val ++ "\n");
throwError "WIP mutual def"
addAndCompileAsUnsafe preDecls
end Term
namespace Command