Additional Expr recognizers needing theory imports

def Lean.Expr.coeTypeSet? (e : Lean.Expr) : Option Lean.Expr

If e is a coercion of a set to a type, return the set. Succeeds either for Set.Elem s terms or {x // x ∈ s} subtype terms.

Equations

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