We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
meta
1 parent 4445958 commit ec9ff12Copy full SHA for ec9ff12
src/Lean/Compiler/MetaAttr.lean
@@ -8,7 +8,7 @@ import Lean.EnvExtension
8
9
namespace Lean
10
11
-builtin_initialize metaExt : TagDeclarationExtension ← mkTagDeclarationExtension
+builtin_initialize metaExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .async)
12
13
/-- Marks in the environment extension that the given declaration has been declared by the user as `meta`. -/
14
def addMeta (env : Environment) (declName : Name) : Environment :=
0 commit comments