runtimeverification/vlsm

Replace `Lib.ListExtras.last_error` with `stdpp.list.last`

Open

#38 创建于 2022年5月3日

在 GitHub 查看
 (0 评论) (1 反应) (0 负责人)Coq (1 fork)auto 404
Proof Engineeringgood first issue

仓库指标

Star
 (5 star)
PR 合并指标
 (PR 指标待抓取)

描述

Before we incorporated stdpp we've been writing developing our own library functions to complement the ones available in stdlib. last_error is one of them, and there are a couple of lemmas proved about it as well some usages throughout the codebase (including some in the indev repository).

Tasks:

  • #39 Refactor the Lib.ListExtras module to define last_error in terms of last and change the existing lemmas about last_error to either be (re)definitions of existing lemmas about last or by proving them using existing results about last
  • #40 (less important, but maybe good to have) Substitute the definitions obtained above with their proper names across the codebase (resisting the temptation to further refactor the code touched by this substitution :-)

贡献者指南