Tests 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.

theorem AnswerLinter.flagged_by_linter (h : True) (b : Nat) : True ↔ 1 + 1 = 2

An exampe of what we want to lint against

theorem AnswerLinter.not_flagged_no_answer_sorry : True → ∀ (x✝ : Nat), 1 + 1 = 2

An non-exampe: we want don't to lint against this case

theorem AnswerLinter.not_flagged_no_arguments : True ↔ 1 + 1 = 2

An non-exampe: we want don't to lint against this case

theorem AnswerLinter.not_flagged_non_prop_answer (h : True) (b : Nat) : sorry = 2 ↔ 1 + 1 = 2

An non-exampe: here answer(sorry) is not a Prop, and not the entire left hand side of the iff.