digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

Step search error in one of the Page412.mmp examples #32

Open david-a-wheeler opened 4 years ago

david-a-wheeler commented 4 years ago

In tutorial Page412.mmp, one of the lines you're supposed to click on (to invoke step search is this:

200:2,100,?:  |- ( ( -. ps -> ph ) -> &W2 )

However, instead of showing a list of options, mmj2 shows: "A-PA-0901 Step 200: Null parse tree for Hyp's formula, this should have been caught!"

As a temporary measure in the mmj2 walkthough I just don't show clicking on that step, since I suspect it will eventually be fixed but I don't want to wait for that before finishing the video.

@digama0 - any idea why it's doing that?