The Exists Implication Linter

Many misformalisations stem from using a pattern of the form ∃ x, P x → Q instead of ∃ x, P x ∧ Q (e.g. when formalising something of the form "there is positive x such that ..."). This is almost always incorrect (and trivial to prove) since it then suffices to pick an x that does not satisfy P. This linter flags occurences of this patter to the user and proposes a corrected syntax.

opaque ExistsImplicationLinter.linter.style.existsImplication : Lean.Option Bool

def ExistsImplicationLinter.forallToAnd (expr : Lean.Expr) : Lean.MetaM Lean.Expr

Changes and expression of the form ∀ (h1 : Prop1) (h2 : Prop2) ..., Propn to Prop1 ∧ Prop2 ∧ ... ∧ Propn.

Equations

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

partial def ExistsImplicationLinter.checkExistsArrow (stx : Lean.Syntax) (e : Lean.Expr) : Lean.MetaM Unit

Checks if an expression contains the pattern ∃ x, P x → Q.

def ExistsImplicationLinter.existsImplicationLinter : Lean.Linter

The existsImplicationLinter detects expressions of the form ∃ a, P a → Q and flags them to the user since those are rarely correct.

Equations

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

opaque ExistsImplicationLinter.zzzThisIsASillyButNecessayNameSeeMyDocstring : Unit

This name is here due to the reappearance of https://github.com/leanprover/lean4/issues/10175.