What function to replace items in List

Stream: new members

[Colin ⚛️]

Can anyone provide me a function that can replace all the A with B in a list ? I tried to use an if statement with pmap or map but it requires Classical.propDecidable which is non computable.

inductive example_type
  | A | B | C | D
open example_type
deriving instance Repr for example_type

def A_to_B (n : example_type) :=
  if n = A then B else n

-- Want a function that takes [A, A, B, C, A, D] and becomes [B, B, B, C, B, D]

[Kyle Miller]

inductive example_type
  | A | B | C | D
  deriving DecidableEq, Repr
open example_type

def A_to_B (n : example_type) :=
  if n = A then B else n

#eval [A, A, B, C, A, D].map A_to_B
-- [example_type.B, example_type.B, example_type.B, example_type.C, example_type.B, example_type.D]

[Kyle Miller]

Or instead of DecidableEq you can use a match:

def A_to_B (n : example_type) :=
  match n with
  | A => B
  | _ => n

[Colin ⚛️]

Thank you!