> On Sunday, August 7, 2022 at 5:05:30 AM UTC+2 [email protected] wrote: > I think you could use "$?" to match any character, and by default it matches > any subexpression so there's no need to use "$*", so the command would be > like: ... > > On Aug 7, 2022, at 8:48 AM, Benoit <[email protected]> wrote: > Thanks "icecream", but my question is about mmj2, not metamath.exe. > Metamath.exe does not parse math expressions, so there is no way to search > for instances of a given expression. (In the sense of a substitution > instance, e.g., "x e. y -> x e. z" is an instance of "ph -> ps"). > Benoît
I realize you asked about mmj2, not metamath.exe, but there's a trick I've used with metamath.exe that *might* be helpful if you're looking for *instances* of a given expression. You can have metamath.exe display the math expressions for each step, then search *that* output for the patterns you want to find (e.g., using grep). You can see an example In the set.mm repo script `scripts/find-repeats`, viewable here: https://github.com/metamath/set.mm/blob/develop/scripts/find-repeats That script sorts instances by how common they are, but the approach seems useful for your case as well. Note: MacOS's grep is really bad & often crashes; the easy solution is to install GNU grep instead. The matches can occasionally match "things I didn't want"... but as a way to quickly search for information, this approach can be quite helpful. --- David A. Wheeler -- 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/292BA8B7-780D-4D85-86CE-765C718529D7%40dwheeler.com.
