Какова будет простая реализация коллекции с неповторяющимися элементами? - PullRequest
Новая
       9

Какова будет простая реализация коллекции с неповторяющимися элементами?

0 голосов
/ 03 ноября 2019

Я знаю, что в стандартной библиотеке есть дерево AVL, но это кажется слишком сложным для моих целей. Функция vanilla отвечает большинству моих требований, за исключением возможности перебирать ключи.

Не похоже, что я строго не знаю, как сделать какое-то предположение, что для каждого элемента в списке нет дубликата - я сделал это в Coq один раз, но я пытаюсь понять, какиспечь его прямо в структуре, и я столкнулся с трудностями. 

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data UniqueList {a} (A : Set a) : Set a
data NotIn {a} {A : Set a} : A → UniqueList A → Set a

data UniqueList A where
  [] : UniqueList A
  _∷_ : ∀ (x : A) (xs : UniqueList A) → NotIn x xs → UniqueList A

data NotIn {a} {A} where
  done : ∀ (x : A) → NotIn x []
  dive : ∀ (x y : A) (ys : UniqueList A) (prf : NotIn y ys) → NotIn x ys → ¬ x ≡ y → NotIn x ((y ∷ ys) prf)

Я думал, что могу попробовать что-то подобное, но это неловко. Любой совет, как с этим бороться?

...