On 5/31/25 04:17, 'Thierry Arnoux' via Metamath wrote:
The grammar parser of metamath-knife might be used to that effect.
I've written up this suggestion (and some other ideas from this thread, such as the idea of maybe using yamma's check in addition) at https://github.com/metamath/set.mm/issues/4864 . We apparently have many of the pieces needed to make this a reality.
-- 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/30057e9a-1977-4b85-a846-00e841033673%40panix.com.
