theorem AnswerLinter.flagged_by_linter (h : True) (b : Nat) : sorry ↔ 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 : sorry ↔ 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.