Documentation

FormalConjectures.Util.Linters.AnswerLinter

The AnswerLinter #

The AnswerLinter is a linter to aid with using answer(sorry) correctly.

source
opaque linter.style.answer_attribute :
Lean.Option Bool
source
def AnswerLinter.contains_early_args (stx : Lean.Syntax) :
Lean.Elab.Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AnswerLinter.stars_with_answer_sorry_iff (stx : Lean.Syntax) :
    Lean.Elab.Command.CommandElabM Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def AnswerLinter.answerLinter :
      Lean.Linter

      The actual linter object

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For