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.
1 parent 923afaf commit c7d42d9Copy full SHA for c7d42d9
src/Lean/Compiler/LCNF/Types.lean
@@ -197,7 +197,7 @@ where
197
| .const declName us =>
198
if (← getEnv).isExporting && isPrivateName declName then
199
-- This branch can happen under `backward.privateInPublic`; restore original behavior of
200
- -- failing here, which is caught and ignore above by `observing`.
+ -- failing here, which is caught and ignored above by `observing`.
201
throwError "internal compiler error: private in public"
202
let .inductInfo _ ← getConstInfo declName | return anyExpr
203
pure <| .const declName us
0 commit comments