标准库中有关联列表吗？

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

标准库中有关联列表吗？

Is there an associative list in the standard library?

agda