Add easy access to guide

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

https://expln.github.io/lamp/latest/index.html

MIT License

12 stars 5 forks source link

Add easy access to guide #72

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

Now that there's a guide at https://lamp-guide.metamath.org it'd be good if the tool made access to it easy.

A few ideas:

A button that creates a new tab & shows the contents
Add a "guide" tab that views lamp-guide.metamath.org (only load it when it's first requested). One advantage of an embedded tab is that if the user has "lots of browser tabs", this would make the guide information clearly paired with the tool.

expln commented 1 year ago

I think tabs become overloaded (especially after adding a proof explorer) . I plan to add a question mark button somewhere on the context selector area when it is expanded. It will open a simple popup with some short text explanations and links to the guide and to the mm-lamp repo.