> On Jan 10, 2025, at 3:17 PM, Sylvain Kerjean <[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 can't create a definition *within* metamath-lamp. However, you can create a text file using any text editor that contains the definition(s) you want. You can then tell metamath-lamp to load it. That's a different process with the same result: You can create definitions, then use your new definitions to prove other things. --- David A. Wheeler -- 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/0D543054-7E5D-4ACE-807C-18EBD6C791A0%40dwheeler.com.
