Hi Marlo, You’re welcome to copy that part of mm-lamp to your proof assistant. Mm-lamp is distributed under the MIT License, which permits reuse and adaptation of the code and design. Moreover, using the same or similar pattern syntax will make it easy for users to switch between multiple proof assistants. I’m glad to hear you’re finding it useful!
- Igor On Saturday, October 11, 2025 at 2:56:52 PM UTC+2 [email protected] wrote: > 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/14a63416-852e-4b67-a796-ba9b7419eb42n%40googlegroups.com.
