expln/metamath-lamp

An assertion tab crashes if the assertion proof contains errors

expln opened this issue · 0 comments

expln commented

Steps to reproduce:

  1. Create a theorem with a valid compressed proof.
  2. Rename one of the labels inside the proof so it doesn't refer to any existing assertion or essential.
  3. Open the tab with this theorem proof - mm-lamp will crash.