runtimeverification/vlsm

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

Open

#39 ouverte le 3 mai 2022

Voir sur GitHub
 (0 commentaires) (0 réactions) (0 assignés)Coq (1 fork)auto 404
Proof Engineeringgood first issue

Métriques du dépôt

Stars
 (5 stars)
Métriques de merge PR
 (Métriques PR en attente)

Description

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

Guide contributeur

Direction de recherche
Stack technique
Domaine
Type d'issue
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Prérequis
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.