From 451ab72eea72e7769546cf34a96e9ff00447bdf9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Jun 2019 10:21:40 -0700 Subject: [PATCH] fix(library/init/lean/attributes): typo --- library/init/lean/attributes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean index 8d225c0bda..575f5533af 100644 --- a/library/init/lean/attributes.lean +++ b/library/init/lean/attributes.lean @@ -326,7 +326,7 @@ match env.getModuleIdxFor decl with | none := (attr.ext.getState env).find decl def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment := -if (env.getModuleIdxFor decl).isNone then +if (env.getModuleIdxFor decl).isSome then Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, declaration is in an imported module") else if ((attr.ext.getState env).find decl).isSome then Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, attribute has already been set")