expln
commented
6 days ago This functionality is available on dev. To mark symbols as adjacent add a modifier before the pattern $+. $ begins a list of modifiers. + stands for "adjacent". There are other modifiers available as well. They are listed in this document https://github.com/expln/metamath-lamp-docs/blob/master/explorer/search_by_pattern.md
As you pointed out, the feature of re-adding flexibility requires much more efforts to implement. So, I am currently not planning to implement it.
david-a-wheeler
Search is easy to use, but it's hard to be specific because it allows 0+ symbols between each symbol.
It'd be nice to have an option (irrelevant in regex) to require that "symbols must be adjacent". If enabled, the pattern specifies a sequence of symbols that must be adjacent (though they could be inside a matching statement). Obviously this is only useful once the search pattern can search on variables (since otherwise there are few useful working patterns).
As a bonus you might add symbols that re-add flexibility. E.g.,
$$for one symbol,$+for 1 or more unspecified symbols, and$*for 0 or more symbols. But that could be done later or never. I'm not sure what the right specifiers should be in this case, and that extra flexibility would require backtracking (or using a DFA which would be complete overkill in this case).