There was a change to the step format a while back to make it more permissive to syntax errors, but it changed the meaning of single colon statements from step:hyps to step:thm. So that means that you have to write 4:3: instead of 4:3 if you want "3" to be interpreted as a hypothesis and not a statement. Like so:
h1000 |- ( ph -> ps ) h200 |- ( ps -> ch ) h30 |- ( ch -> th ) 3:200: |- ( ph -> ( ps -> ch ) ) 4:3: |- ( ( ph -> ps ) -> ( ph -> ch ) ) qed:1000,4: |- ( ph -> ch ) The hypothesis steps don't need the colons because they have no hypotheses (so h1000 will automatically be turned into h1000:: ). Mario On Thu, Dec 26, 2019 at 8:59 PM David A. Wheeler <[email protected]> wrote: > I have a strange problem with mmj2's file "PA301.mmp" - anyone have > any idea what's up? > > Background: > I'm doing a dry run of the mmj2 "PATutorial" files. However, when I try to > unify (control-U) file PA301.mmp, I get the following error instead of a > unification: > > E-PA-0348 Theorem sylClone Step 3: Invalid Ref = 200 on derivation proof > step. Does not specify a valid statement in the Metamath file that was > loaded. You can leave Ref blank to allow Unify to figure it out for you. > Proof Text input reader last position: Source Id: Proof Text Line: 21 > Column: 3 > > The error is on this line: > 3:200 |- ( ph -> ( ps -> ch ) ) > which refers back to this hypothesis: > h200 |- ( ps -> ch ) > > That should work, but it doesn't. Changing "3:200" to "3:h200" doesn't > work either > (though that shouldn't be needed). > > Anyone else seen this? Full file contents below. > > --- David A. Wheeler > > ======================================= > > $( <MM> <PROOF_ASST> THEOREM=sylClone LOC_AFTER=a2i > * Page301.mmp > Have a careful look at the "Step:Hyp:Ref" field at the start of each > proof step below. Notice especially how: > - Hypothesis Step Numbers are prefixed with 'h' > - Step Numbers are not in numeric order(!), but are unique > - Ref Labels are blank > - Trailing ":"s are optional, for your convenience > - Blanks are not permitted inside a "Step:Hyp:Ref" (making things > easier for the programmers) > - the final step "number" is "qed" (also for the convenience of > the programmer...) > > OK, now press Ctrl-U and see what happens to the Step:Hyp:Ref fields. > (Use Edit/Undo -- twice -- to retry and look again.) > > h1000 |- ( ph -> ps ) > h200 |- ( ps -> ch ) > h30 |- ( ch -> th ) > 3:200 |- ( ph -> ( ps -> ch ) ) > 4:3 |- ( ( ph -> ps ) -> ( ph -> ch ) ) > qed:1000,4 |- ( ph -> ch ) > > *OK, proceed to the next Tutorial page (Page302.mmp)! > $) > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/E1ikeuB-0007Zn-I1%40rmmprod07.runbox > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvbkhga9G5KD24xgEyQPkTgPopdFm2DmjcDkeZdsTA%2BiQ%40mail.gmail.com.
