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

feat: "compile" 'extern' axioms

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-13 06:57:02 -08:00
parent f6e5b13591
commit b6bb31a131
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Compiler/Util.lean
View file

@ -74,6 +74,7 @@ private def getDeclNamesForCodeGen : Declaration → List Name
| Declaration.defnDecl { name := n, .. } => [n]
| Declaration.mutualDefnDecl defs => defs.map fun d => d.name
| Declaration.opaqueDecl { name := n, .. } => [n]
| Declaration.axiomDecl { name := n, .. } => [n] -- axiom may be tagged with `@[extern ...]`
| _ => []
def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=

2
src/Lean/Elab/Declaration.lean
View file

@ -82,6 +82,8 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
Term.ensureNoUnassignedMVars decl
addDecl decl
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
if isExtern (← getEnv) declName then
compileDecl decl
Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
/-