From b6bb31a131e5ce6502e987a2ff5fa1db2af42e07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Jan 2021 06:57:02 -0800
Subject: [PATCH] feat: "compile" 'extern' axioms

---
 src/Lean/Compiler/Util.lean    | 1 +
 src/Lean/Elab/Declaration.lean | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean
index 3bf806cf3a..76e67f585c 100644
--- a/src/Lean/Compiler/Util.lean
+++ b/src/Lean/Compiler/Util.lean
@@ -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 :=
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 40465032ea..1003aaeb84 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -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
 
 /-