diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index c19ae21b86..4afd5cb05b 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -26,6 +26,7 @@ registerParametricAttribute `init "initialization procedure for global reference decl ← getConstInfo declName; match attrParamSyntaxToIdentifier stx with | some initFnName => do + initFnName ← resolveGlobalConstNoOverload initFnName; initDecl ← getConstInfo initFnName; match getIOTypeArg initDecl.type with | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO `") diff --git a/tests/compiler/init.lean b/tests/compiler/init.lean index af07656556..66bc172bee 100644 --- a/tests/compiler/init.lean +++ b/tests/compiler/init.lean @@ -1,5 +1,7 @@ new_frontend +namespace Foo + initialize ref : IO.Ref Nat ← IO.mkRef 10 initialize vals : IO.Ref (Array String) ← IO.mkRef #[] @@ -20,6 +22,9 @@ initialize initialize registerVal "foo" +end Foo +open Foo + def main : IO Unit := do IO.println "hello world" IO.println (← ref.get)