Search: Optionally require symbols to be adjacent (low priority)

[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).

[expln]

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]

Awesome! Let me know when that's in a released version, and I'll update the doc to match.

My primary desire now is #77 (full unification) but obviously that's a subtle algorithm that is much harder :-).

[expln]

Awesome! Let me know when that's in a released version, and I'll update the doc to match.

Sure. I am going to release what currently is in the dev version after some testing. I also created a CHANGELOG.md, so it should be easier to track changes now.

My primary desire now is #77 (full unification) but obviously that's a subtle algorithm that is much harder :-).

Yeah, I remember that issue :)

[expln]

@david-a-wheeler

Hi David, this feature is released in version 25.

[david-a-wheeler]

1. Awesome! Thank you so much!
2. Uh oh, I'd better get moving to update the guide :-). A happy "problem".

[expln]

Thank you!