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.
