Re: [Metamath] LAMP axiom/definition

['David A. Wheeler' via Metamath]

> On Jan 11, 2025, at 6:27 PM, Sylvain Kerjean <sylvain.kerjea...@gmail.com> 
> 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 metamath+unsubscr...@googlegroups.com.
To view this discussion visit 
https://groups.google.com/d/msgid/metamath/ADCEBE0C-FD55-4A2A-B9A8-773CB9534AE3%40dwheeler.com.