如何解决Agda Vec如何过滤出元素
嗨,我认为我不太了解如何使用Vec.filter
中的Data/Vec.agda
。
我知道如何“过滤”(保留)向量中的元素
filterProof : v.filter (λ e → e ≟ 2) (2 v.∷ v.[]) ≡ (2 vb.∷ vb.[])
filterProof = refl
但是我不确定如何“滤出”元素。
filterProof : v.filter (λ e → e ? 2) (2 v.∷ v.[]) ≡ vb.[]
filterProof = refl
我不确定?
的位置。
我知道类型必须为Relation.Nullary.Dec
,但不确定如何使用e ≠ 2
中可用的内容来表达Relation.Nullary.Dec
。
我还想知道为什么Vec.filter
不像Bool
那样使用Relation.Nullary.Dec
而不是List.filter
进行过滤。
谢谢!
解决方法
您可以将谓词的决策过程转换为否定的决策过程:
open import Relation.Nullary
dec-¬ : ∀ {a} {P : Set a} → Dec P → Dec (¬ P)
dec-¬ (yes p) = no λ prf → prf p
dec-¬ (no ¬p) = yes ¬p
这当然意味着您也可以取消可决定的关系:
open import Relation.Binary
module _ {a} {A B : Set a} {ℓ} where
neg : REL A B ℓ → REL A B ℓ
neg R x y = ¬ (R x y)
decidable-neg : ∀ {R : REL A B ℓ} → Decidable R → Decidable (neg R)
decidable-neg dec x y = dec-¬ (dec x y)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。