如何解决Agda Vec.filter给出Vec≤,如何返回Vec?
我注意到Vec.filter
的签名是
filter : ∀ {n} → Vec A n → Vec≤ A n
为了返回Vec
,我可以仅使用
padRight : ∀ {n} → A → Vec≤ A n → Vec A n
或
padLeft : ∀ {n} → A → Vec≤ A n → Vec A n
?
理想情况下,我想找回一个Vec
,它的长度等于Vec
的初始长度减去已滤除的元素数量(而不是填充元素已被滤除)。
谢谢!
解决方法
如果您查看the definition of Vec≤
,将会发现它已经完全符合您的要求:
record Vec≤ (A : Set a) (n : ℕ) : Set a where
constructor _,_
field {length} : ℕ
vec : Vec A length
.bound : length ≤ n
所以vec
中的Vec≤ A n
是“正常” Vec A length
,对于某些length
小于n
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。