IsLaterCommand — Mathlib

Lean4
/-- `IsLaterCommand` is an `IO.Ref` that starts out being `false`.
As soon as a (non-import) command in a file is processed, the `deprecated.module` linter`
sets it to `true`.
If it is `false`, then the `deprecated.module` linter will check for deprecated modules.

This is used to ensure that the linter performs the deprecation checks only once per file.
There are possible concurrency issues, but they should not be particularly worrying:
* the linter check should be relatively quick;
* the only way in which the linter could change what it reports is if the imports are changed
  and a change in imports triggers a rebuild of the whole file anyway, resetting the `IO.Ref`.
-/
@[init initFn✝, ]
opaque IsLaterCommand : IO.Ref Bool
Похожие утверждения