That’s right, you cannot create axioms and definitions in mm-lamp. You can only edit/develop proofs. But that should not be a problem, because you can manually (using a usual text editor) add your new axioms and definitions to an existing database. Or, as David pointed out, it will be handy to keep new axioms in a separate file/files and load it/them together with the main database. In addition to the metamath-lamp guide, you can see an example of how you can organize files in this video https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing . At 18:13 it is shown how to load two files.
If you keep your axioms in a separate file, you can include the main database with the include statement, for example [ set.mm ], at the beginning of your file. Then you will be able to validate your file with a single command in metamath.exe. You will need to pass only your file to metamath.exe. Metamath.exe will automatically load all databases specified in include statements at the beginning of your file. A similar question was posted on GitHub https://github.com/expln/metamath-lamp/issues/200 . There is an answer which shows that you still can use mm-lamp to validate syntax of your new axioms and provides more details on this topic. - Igor On Monday, January 13, 2025 at 6:23:30 PM UTC+1 David A. Wheeler wrote: > > > > On Jan 11, 2025, at 6:27 PM, Sylvain Kerjean <[email protected]> > wrote: > > > > Is it possible to add an axiom or definition in lamp ? It seems in the > editor, you can only edit a proof, but you can't add new definitions. > Though lamp is able to read them from a database. > > Metamath-lamp allows you to select multiple sources as input. It will then > load them in order. > > I usually create a small local file with additional axioms & definitions. > You can then load the "main" database up to where you want to start, then > load the other file with your additional axioms/definitions. You could > also post that local file on the web, > and load it that way. > > More info in the metamath-lamp guide here: > > https://lamp-guide.metamath.org/#loading-source-metamath-databases-to-create-the-proof-context > > --- 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/cba5e418-b95d-4bb6-a601-929164e244a4n%40googlegroups.com.
