标准库中有关联列表吗

Question

我没有足够的信心来尝试证明关于AVL树的属性，所以我想尝试更简单的方法。我可以自己实现它，但如果它已经藏在图书馆的某个地方，我不想花时间这样做。

Answer 1

您可以使用一个对列表，然后可以通过Any对成员关系的概念进行编码。

一个非常基本的库的位：

open import Data.List.Base using (List)
open import Data.List.Relation.Unary.Any
open import Data.Maybe
open import Data.Product
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
AssocList : Set → Set → Set
AssocList A B = List (A × B)
private
variable
A B : Set
_∈_ : A → AssocList A B → Set
a ∈ abs = Any ((a ≡_) ∘ proj₁) abs
module Decidable {A : Set} (_≟_ : Decidable {A = A} _≡_) where
_∈?_ : Decidable (_∈_ {A} {B})
a ∈? abs = any ((a ≟_) ∘ proj₁) abs
_‼_ : (abs : AssocList A B) (a : A) → Maybe B
abs ‼ a with a ∈? abs
... | yes p = just (proj₂ (lookup p))
... | no ¬p = nothing