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/ed36024a-2d91-4039-b69f-5469bf3a0ef9n%40googlegroups.com.
