Hi Sylvain,
No, it is not possible to add axioms/definitions in mm-lamp. However, you can use mm-lamp to construct axioms/definitions and then copy them to an existing database. Please see this thread, which contains more details on this topic: https://groups.google.com/g/metamath/c/yvjanSQf3iQ - Igor On Friday, January 17, 2025 at 6:07:06 AM UTC+1 [email protected] wrote: > I wonder if it is possible to add a definition in Lamp? Or is it just > intendend to prove statement from an existing database ? -- 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/e902a1a2-61e5-45b3-a53b-352dcfc6af6an%40googlegroups.com.
