/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtil.Linters.AnswerLinter
public import FormalConjecturesUtil.AnswerTests for the answer linter
This file contains test cases for the AnswerLinter, verifying that it correctly flags
theorems with early arguments when answer(sorry) is the left-hand side of an iff,
and does not flag theorems without answer(sorry) or without early arguments.
public sectionset_option warn.sorry falsenamespace AnswerLinter
/--
warning: Move the quantifiers outward:
instead of
theorem foo (bar : ℕ) (baz : ℕ) : answer(sorry) ↔ ...
likely the intention was
theorem foo : answer(sorry) ↔ ∀ᵉ (bar : ℕ) (baz : ℕ), ...
Note: This linter can be disabled with set_option linter.style.answer_attribute false
#guard_msgs inAn exampe of what we want to lint against
theorem flagged_by_linter (h : True) (b : Nat) : answer(sorry) ↔ 1 + 1 = 2 := h:Trueb:Nat⊢ True ↔ 1 + 1 = 2
All goals completed! 🐙#guard_msgs inAn non-exampe: we want don't to lint against this case
theorem not_flagged_no_answer_sorry (_ : True) (_ : Nat) : 1 + 1 = 2 := x✝¹:Truex✝:Nat⊢ 1 + 1 = 2
All goals completed! 🐙#guard_msgs inAn non-exampe: we want don't to lint against this case
theorem not_flagged_no_arguments : answer(sorry) ↔ 1 + 1 = 2 := ⊢ True ↔ 1 + 1 = 2
All goals completed! 🐙#guard_msgs in
An non-exampe: here answer(sorry) is not a Prop, and not the entire left
hand side of the iff.
theorem not_flagged_non_prop_answer (h : True) (b : Nat) : answer(sorry) = 2 ↔ 1 + 1 = 2 := h:Trueb:Nat⊢ sorry = 2 ↔ 1 + 1 = 2
All goals completed! 🐙end AnswerLinter