leanprover-community/ProofWidgets4

feature request: widget to display the docstring of the current lemma

Offen

#70 geöffnet am 15.07.2024

Auf GitHub ansehen
 (0 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)Lean (45 Forks)auto 404
enhancementhelp wanted

Repository-Metriken

Stars
 (219 Sterne)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

For interactive proof it can be helpful to have the docstring for the lemma currently being proven pretty-printed in the infoview alongside the tactic state. This can be especially useful when the docstring includes sources for TikZ diagrams. These should be rendered correctly in the infoview.

Contributor Guide

Research-Richtung
Erkunde, wie ProofWidgets4 Widgets im Infoview rendert. Studiere, wie man auf den Docstring des aktuellen Lemmas aus der Lean Umgebung zugreift. Schau dir Beispiele bestehender Widgets an, um zu verstehen, wie Text und Bilder (wie TikZ) gerendert werden. Implementiere dann ein neues Widget, das den Docstring anzeigt.
Tech Stack
Keine
Domain
developer experience
Issue Type
Funktion
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-2 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Frisch
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
Lean 4ProofWidgets4
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
30