Improved pattern search in metamath-lamp

[Igor Ieskov]

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 version of metamath-lamp only. This document 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, or create a new issue in mm-lamp repository.

-
Igor

[Marlo Bruder]

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

[Igor Ieskov]

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