我能够轻易获得密钥列表如下:如何获取Data.AVL.Tree中的值列表?
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_)
module AVL-Tree-Functions
{ k v ℓ } { Key : Set k }
(Value : Key → Set v)
{ _<_ : Rel Key ℓ }
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
where
open import Data.AVL Value isStrictTotalOrder public
open import Data.List.Base
open import Function
open import Data.Product
keys : Tree → List Key
keys = Data.List.Base.map proj₁ ∘ toList
但我不如何指定返回值的列表的功能类型明确。这是我第一次尝试:
-- this fails to typecheck
values : Tree → List Value
values = Data.List.Base.map proj₂ ∘ toList
与此相关的,我也感到困惑的Value
在Data.AVL声明。用(Value : Key → Set v)
,它看起来像树中每个值的类型取决于密钥?或类似的东西。那么我想,proj₂将返回Set v
类型的东西,所以我尝试这样做:
-- this also fails to typecheck
values : Tree → List (Set v)
values = Data.List.Base.map proj₂ ∘ toList
但是,这并不工作,要么(它失败,不同的错误)。请显示如何从Data.AVL.Tree获取值的列表(或解释为什么不可能)。奖金:解释为什么我的两次尝试失败。
P.s.这是使用Agda版本2.4.2.3和agda-stdlib。
这是很难在gallais'和user3237465的答案之间做出决定。我跟user3237465去了,因为'索引列表'的方法足以解决我的特殊问题。非常感谢,并且为了这个出色的,内容丰富的答案已经成为gallais的代表。 – m0davis