How to get the associated attribute given membership

Stream: Is there code for X?

[Schrodinger ZHU Yifan]

structure AType where
  mk::
  something : Unit

@[reducible]
def Map (f : (String × AType) → α) (x : List (String × AType)) : List α :=
  match x with
  | [] => []
  | h :: xs => (f h) :: Map f xs

abbrev Names δ := Map (·.fst) δ
abbrev Attribute δ := Subtype (· ∈ (Names δ))

def ATypeOf {δ} (x : Attribute δ) : AType :=
  -- how to write this?

[Adam Topaz]

your code doesn't work for me. please provide a #mwe

[Kyle Miller]

It didn't work for me either, and I was going to ask for an #mwe too, but I'm guessing this is what you're looking for:

import Std

set_option autoImplicit true

variable {AType : Type}

@[reducible]
def Map (f : (String × AType) → α) (x : List (String × AType)) : List α :=
  match x with
  | [] => []
  | h :: xs => (f h) :: Map f xs

abbrev Names (δ : List (String × AType)) := Map (·.fst) δ
abbrev Attribute (δ : List (String × AType)) := Subtype (· ∈ (Names δ))

def ATypeOf {δ : List (String × AType)} (x : Attribute δ) : AType :=
  match δ, x with
  | [], x => by
    have := x.property
    simp [Names, Map] at this
  | h :: xs, x =>
    if he : h.1 = x.1 then
      h.2
    else
      ATypeOf (δ := xs) ⟨x.1, by
        have := x.property
        simp [Names, Ne.symm he] at this
        exact this⟩

[Schrodinger ZHU Yifan]

Thanks. AType is just some other structure. It is irrelevant so I did not add it in. I have updated the code to include one.