runtimeverification/vlsm
GitHub で見るReplace `Lib.ListExtras.last_error` with `stdpp.list.last`
Open
#38 opened on 2022年5月3日
Proof Engineeringgood first issue
Repository metrics
- Stars
- (5 stars)
- PR merge metrics
- (PR metrics pending)
説明
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.ListExtrasmodule to definelast_errorin terms oflastand change the existing lemmas aboutlast_errorto either be (re)definitions of existing lemmas aboutlastor by proving them using existing results aboutlast - #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 :-)