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/CAAfCLngx__m6016YiB82nF-8AVZ_mBOUsFv-HO%2BA%2BAYqNMBkZQ%40mail.gmail.com.
