Равенство в определениях (разрешимое равенство? Например, заменить элементы в списке)

Я пытаюсь изучить lean и хочу определить функцию замены, которая принимает два элемента x и y и заменяет каждое вхождение x с y в заданном списке.

Я попытался определить это так:

def replace {α : Type}: α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs

Это дает мне следующую ошибку:

error: failed to synthesize type class instance for
α : Type,
replace : α → α → list α → list α,
a b x : α,
xs : list α
⊢ decidable (a = x)

Моя проблема в том, что я не могу использовать равенство для типа α, поэтому я думаю, что мне нужно ограничить α каким-то типом класса, где равенство разрешимо (как в Haskell). Как я могу это сделать?

Мой текущий обходной путь состоит в том, чтобы использовать функцию равенства в качестве параметра:

def replace {α : Type}: (α -> α -> bool) -> α -> α -> list α -> list α
| eq a b [] := []
| eq a b (x::xs) := (if eq a x then b else x) :: replace eq a b xs

typeclass lean
person Peter Zeller    schedule 14.11.2017    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете взять разрешимое равенство α в качестве аргумента класса типа, например:

def replace {α : Type} [decidable_eq α] : α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs

#eval replace 2 3 [2, 2, 5, 6, 3, 2]

Квадратные скобки означают, что экземпляр класса типов должен выводиться путем разрешения класса типов.

person Rob Lewis    schedule 14.11.2017