Ah, so the $d statement is required. In the testcase that I was using, I
failed to notice the $d statement above the block of lemmas that shared a
${ frame, and the updated code also failed to store the $d variable pairs
where it was supposed to; so I have a different type of bug that I thought
I did.
On Thursday, June 6, 2019 at 10:00:55 PM UTC-5, Norman Megill wrote:
>
> It is required by the spec, in the place I mentioned in my previous post.
> If you comment out a $d with a dummy variable, it will cause proof
> verification to fail in metamath.exe and most others. Hmm is the only one
> I recall that assumes implicit $d's for dummy variables, but as Mario says
> it's non-conforming.
>
> Norm
>
--
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/5de69e38-f26d-435a-af25-68101025e15c%40googlegroups.com.
