getMemType — Mathlib

Lean4
/-- If `e` is of the form `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, or `x ∈ (A : Multiset α)`,
return `some α`, otherwise `none`. -/
def getMemType {m : Type → Type} [Monad m] [MonadError m] (e : Expr) : m (Option Expr) := do
  match e.getAppFnArgs with
  | (``Membership.mem, #[_, type, _, _, _]) =>
    match type.getAppFnArgs with
    | (``List, #[α]) =>
      return α
    | (``Multiset, #[α]) =>
      return α
    | (``Finset, #[α]) =>
      return α
    | _ =>
      throwError"Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, \
                                 or `x ∈ (A : Multiset α)`"
  | _ =>
    return none
Похожие утверждения