[Lamp] add axiom/definition ?

[Sylvain Kerjean]

I wonder if it is possible to add a definition in  Lamp? Or is it just intendend to prove statement from an existing database ?

[Igor Ieskov]

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

[David A. Wheeler]

> On Jan 10, 2025, at 3:17 PM, Sylvain Kerjean <sylvain....@gmail.com> 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