Module docstring
{"# Additional Expr recognizers needing theory imports
"}
Lean.Expr.coeTypeSet?
definition
(e : Expr) : Option Expr
Full source
/-- 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. -/
def coeTypeSet? (e : Expr) : Option Expr := do
if e.isAppOfArity ``Set.Elem 2 then
return e.appArg!
else if e.isAppOfArity ``Subtype 2 then
let .lam _ _ body _ := e.appArg! | failure
guard <| body.isAppOfArity ``Membership.mem 5
let #[_, _, inst, .bvar 0, s] := body.getAppArgs | failure
guard <| inst.isAppOfArity ``Set.instMembership 1
return s
else
failureInformal description
Given a Lean expression `e`, this function checks if `e` represents a coercion of a set to a type. It succeeds if `e` is either a `Set.Elem s` term or a `{x // x ∈ s}` subtype term, and in either case returns the underlying set `s`. Otherwise, it returns `none`.