Exciting news! I have been thinking about implementing metamath-lamps "search by pattern" in my own upcoming proof assistant mmt1 (since mmt1s "search by parse tree" is still relatively weak). I probably won't have time to do so before my October release date, but I just wanted to ask now: Would it be OK for you if I copy the design of your algorithm in the future?
Best regards, Marlo Bruder On Saturday, October 11, 2025 at 12:32:12 PM UTC+2 [email protected] wrote: > Hi all, > > An improved version of pattern search has recently become available in > metamath-lamp. The new version gives more freedom in specifying what you > want to find. Currently it is available in the dev > <https://expln.github.io/lamp/dev/index.html> version of metamath-lamp > only. This document > <https://github.com/expln/metamath-lamp-docs/blob/master/mm_lamp_versions/dev/explorer/search_by_pattern_v2.md> > > describes the new pattern search. > > If you have any questions, or you find an issue or bug, please feel free > to reply either in this conversation thread, or in this GitHub issue > <https://github.com/expln/metamath-lamp/issues/237>, or create a new > issue in mm-lamp repository > <https://github.com/expln/metamath-lamp/issues>. > > - > Igor -- 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 visit https://groups.google.com/d/msgid/metamath/cbcbcada-70d7-42da-a06c-bf0f8be13a35n%40googlegroups.com.
