@[specialize #[0]]

partial def Lean.Expr.hasUnusedForallBindersWhere (p : BinderInfo → Expr → Bool) (e : Expr) : Bool

Tests if any of the binders of (x₀ : A₀) → (x₁ : A₁) → ⋯ → X which satisfy p Aᵢ bi (with bi the binderInfo) are unused in the renainder of the type (i.e. in (xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X).

Note that the argument to p may have loose bvars. This is a performance optimization.

This function runs cleanupAnnotations on each type suffix (xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X before examining it.

We see through lets, and do not report if any of them are unused.