如何解决表明在对Vec进行过滤之后,该Vec不包含任何满足过滤谓词的元素
我想证明打来电话
DeleteTodo : ∀ {n} → (Vec Todo n) → ℕ → (Vec Todo n)
DeleteTodo todos id' =
padRight
record
{ id = 1 -- argmax (λ todo → λ e → e) todos) + 1
; completed = false
; text = ""
}
(v.filter (λ todo → Todo.id todo ≟ id') todos)
在Vec
的{{1}}上的没有任何Todo
的id = id'。
因为Todo
返回了filter
,所以我使用Vec≤
将padRight
投射回了Vec≤
。
语句如下:
Vec
基本上,尝试将DeleteTodoRemoveTodoById :
∀ {n : ℕ} (id' : ℕ) (todos : Vec Todo n) →
padRight
record
{ id = 1 -- argmax (λ todo → λ e → e) todos) + 1
; completed = false
; text = ""
}
(v.filter (λ todo → Todo.id todo ≟ id') (DeleteTodo todos id'))
≡ DeleteTodo todos id'
DeleteTodoRemoveTodoById id' todos = ?
应用到已删除具有给定ID的待办事项的filter
上,将得到与调用todos
相同的结果。
我想知道这种方法是否有意义,或者是否有更简单的方法来证明DeleteTodo
删除所有具有给定ID的待办事项。
谢谢!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。