1
私はleanを学び、二つの要素x
とy
を取り、与えられたリストでy
でx
のすべての発生を置き換える置き換え機能を、定義したいしようとしています。平等(決定可能平等?例えば、リスト内の要素を置き換える)
私はこのようにそれを定義しようとしました:
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