simproc for ∃ a', ... ∧ a' = a ∧ ...

This module implements the existsAndEq simproc that checks whether P a' has the form ... ∧ a' = a ∧ ... or ... ∧ a = a' ∧ ... for the goal ∃ a', P a'. If so, it rewrites the latter as P a.

def existsAndEq.findImpEqProof (p : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

For an expression p of the form fun (x : α) ↦ (body : Prop), checks whether body implies x = a for some a, and constructs a proof of (∃ x, p x) = p a using exists_of_imp_eq.

Equations

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

partial def existsAndEq.findImpEqProof.go (x h : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Traverses the expression h, branching at each And, to find a proof of x = a for some a.

def existsAndEq : Lean.Meta.Simp.Simproc

Checks whether P a' has the form ... ∧ a' = a ∧ ... or ... ∧ a = a' ∧ ... in the goal ∃ a', P a'. If so, rewrites the goal as P a.

Equations

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