functions out of List types

Stream: Is there code for X?

[Elif Uskuplu]

I have couple of questions about following #mwe. How can I fix the errors? Also, is there any way to define dom_B function?

import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Basic

open List

section
variable (A B : Type)

def dom_A : (List (A × B)) → (Finset A)
| [] => ∅
| ((x, _) :: L') => {x} ∪ (dom_A L') -- Error message: failed to synthesize instance Union (Finset A)

def dom_B (L : List (A × B)) : (dom_A L) → B := by sorry
/-
Error message:
application type mismatch
  dom_A L
argument
  L
has type
  List (A × B) : Type
but is expected to have type
  Type : Type 1-/

end

[Kyle Miller]

It's probably that you need DecidableEq A to get the Union for Finset A`.

[Kyle Miller]

For the second error, notice that you made A and B be explicit

[Elif Uskuplu]

@Kyle Miller In my real code, I don't have the second error. This was for #mwe, but I see the reason, thanks. I got it the first one. What about dom_B definition? Do you have any suggestion?

[Kyle Miller]

This seems to work:

variable {A B : Type} [DecidableEq A]

def dom_A (L : List (A × B)) : Finset A := (L.map Prod.fst).toFinset

def dom_B (L : List (A × B)) (a : dom_A L) : B :=
  match L, a with
  | [], ⟨_, h⟩ => by simp [dom_A] at h
  | (a, b) :: L, ⟨a', h⟩ =>
    if ha : a = a' then
      b
    else
      dom_B L ⟨a', by simpa [dom_A, Ne.symm ha] using h⟩

[Kyle Miller]

Your dom_A is fine, but it's worth using builtin functions I think.

[Elif Uskuplu]

@Kyle Miller It worked perfectly, thanks.