leanprover-community/ProofWidgets4

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

Aperta

#70 aperta il 15 lug 2024

Vedi su GitHub
 (0 commenti) (0 reazioni) (0 assegnatari)Lean (45 fork)auto 404
enhancementhelp wanted

Metriche repository

Star
 (219 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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.

Guida contributor

Direzione di ricerca
Esplora come ProofWidgets4 renderizza i widget nell'infoview. Studia come accedere alla docstring del lemma corrente dall'ambiente Lean. Guarda esempi di widget esistenti per capire come rendere testo e immagini (come TikZ). Poi implementa un nuovo widget che visualizzi la docstring.
Tech stack
Nessuno
Dominio
developer experience
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Nuova
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Lean 4ProofWidgets4
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30