정의의 평등 내가 <a href="https://leanprover.github.io/" rel="nofollow noreferrer">lean</a>를 배우려고 노력하고 두 가지 요소가 필요 <code>x</code> 및 <code>y</code> 주어진 목록에 <code>y</code>와 <code>x</code>의 모든 발생을 대체하는 대체 함수를 정의 할 수 있어요

Question

(decidable 평등? 예를 들어, 목록에서 요소를 대체).

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) 

내 문제는 내가 유형 α에 대한 평등을 사용할 수 없다는입니다, 그래서 것 같아요 α을 평등을 결정할 수있는 일종의 클래스로 제한해야합니다 (하스켈처럼). 어떻게해야합니까?

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 

Answer 1

당신은이 같은 유형의 클래스 인수로 α의 decidable 평등을 수행 할 수 있습니다 :

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] 

나의 현재 해결는 매개 변수로 평등의 기능을하는 것입니다 대괄호는 유형 클래스의 인스턴스가 유형 클래스 분석에 의해 유추되어야 함을 나타냅니다.