Commit 2023-03-17 10:29 81530d1e

View on Github →

feat: add logLintIf (#2933)

  • This logs a linter error only if the option is set
  • I thought that was the behavior of logLint already, but that was false. This still seems to be a good option to have.
  • Part of the reason I was mislead is that Lean.Linter.logLint (and Lean.logWarningAt) have an unused MonadOptions argument

Estimated changes