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 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: > > search * "$?$? -> ( E. $? ( $?$? /\ $?$? ) ->" > > But when I try that, there's no results. Nevertheless there are results for > search * "( E. $? ( $?$? /\ $?$? ) ->" > [image: image.png] > > On Sat, Aug 6, 2022 at 7:03 PM Benoit <[email protected]> wrote: > >> Thanks Glauco. I tried several variations but none work for me either... >> On Saturday, August 6, 2022 at 10:42:14 PM UTC+2 Glauco wrote: >> >>> Reading the help (see below the relevant part) it should be (but it >>> doesn't work, for me): >>> >>> InWhat: $ap >>> Part: Formulas >>> Format: ParseStmt >>> Oper: <= (this if you want "contained" instances, as you wrote above) >>> ForWath: ( ph -> ( E. x ( ph /\ ps ) -> ch ) ) (it wants a >>> "parsable" stmt, otherwise it returns an error) >>> >>> >>> From the help: >>> >>> <snip> >>> The other two Formats, 'ParseExpr' and 'ParseStmt' operate on syntactic >>> parse trees (and so are restricted to formula objects...) When using >>> these >>> Formats the contents of the ForWhat field are parsed into syntax trees >>> for >>> use in the searching process. >>> <snip> >>> * ParseStmt : a ParseStmt search term is parsed to construct a parse >>> tree for >>> the statement (in set.mm it must be a wff). The statement's parse >>> tree is >>> then used in a unification-like process to search for a match with a >>> formula >>> parse tree. The precise match requirement is given by the Oper field -- >>> please refer to the Oper help text for details. Note: ParseExpr search >>> terms >>> must not begin with a statement code constant (i.e. "|-") and must not >>> contain Work Variables. Example: "( ph -> ps )". >>> >>> >>> (there's a copypaste mistake: "Note: ParseExpr" should be Note: >>> ParseStmt ) >>> >>> >>> Il giorno sabato 6 agosto 2022 alle 18:24:51 UTC+2 Benoit ha scritto: >>> >>>> Since mmj2 can parse expressions, there might be a way to look for >>>> expressions which contain instances of a given expression ? >>>> >>>> For example, how do I search all assertions which contain as a >>>> subexpression an instance of "ph -> ( E. x ( ph /\ ps ) ->" ? >>>> >>>> Thanks, >>>> Benoît >>>> >>> -- >> 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/f7ea3431-e5d8-4cc6-92a5-b99ccdaed7bbn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/f7ea3431-e5d8-4cc6-92a5-b99ccdaed7bbn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/63765d98-b424-46ca-a255-ec734a096320n%40googlegroups.com.
