issues
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
11
stars
4
forks
source link
An assertion tab crashes if the assertion proof contains errors
#184
Open
expln
opened
7 months ago
expln
commented
7 months ago
Steps to reproduce:
Create a theorem with a valid compressed proof.
Rename one of the labels inside the proof so it doesn't refer to any existing assertion or essential.
Open the tab with this theorem proof - mm-lamp will crash.
Steps to reproduce: