runtimeverification/vlsm

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

Open

#39 geöffnet am 3. Mai 2022

Auf GitHub ansehen
 (0 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)Coq (1 Fork)auto 404
Proof Engineeringgood first issue

Repository-Metriken

Stars
 (5 Stars)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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

Contributor Guide

Research-Richtung
Tech Stack
Domain
Issue Type
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Voraussetzungen
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.