On 1/8/20 5:01 AM, Mario Carneiro wrote:
I would have completely removed the "?" but it breaks a lot of
backward compatibility. It is currently only useful for the "step
search": if you double click on "step:: |- foo" then it will search
only for proofs of |- foo with no assumptions, and if you double click
"step:?: |- foo" it will search for proofs of foo with possibly
additional hypotheses.
The ? is still useful in telling mmj2 which hypotheses to fill in. For
example, if I have a step 500 and I want to say
510:500:syl2anc
and have mmj2 fill in the other two hypotheses. Before typing control-U
I can modify that to be:
510:?,?,500:syl2anc
or
510:500,?,?:syl2anc
before writing unify.
I just tried this with mmj2 2.5.3 as of 23-Sep-2019 (as reported in the
About box).
--
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/6ca7f932-4475-3dcc-d66b-d42c2296a63c%40panix.com.
