search

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

Enable display of variable types (low priority) #110

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

I'd love to expand controls over what explorer tab can show, in particular variable types ($f).

Currently there's a single "Assertion type" which can be "Axioms", "Theorems", or "All" (which really just means axioms & theorems). It'd be awesome to also be able to show "Variable types" (aka $f aka "floating" assertions. I suspect it'd be better to have a checkbox (on/off) for each of axioms, theorems, and variable types. This would also imply that variable type labels could be displayed and clicked on, e.g., this set.mm statement:

 $( Let variable ` ph ` be a wff. $)
  wph $f wff ph $.

Would be displayed in the explorer as something like (the text after > is on open):

Variable Type wph > [ Let variable ` ph ` be a wff. ]
wff ph

Clicking on the wph would produce a tab showing its description followed by Typecode VariableName, e.g.,:

Variable Type wph
Let variable ` ph ` be a wff.

wff ph

These would also be clickable in other tables where syntax is shown.

The idea is that, since it already supports showing syntax tables, it'd make more sense to go down to declaring the types of each symbol. This would eliminate the mystery of "how does it determine the type of ph ?" and similar.