Thanks for your answer. I should have better looked at the settings "+" :) Another question : I try to follow the 'Théorie des ensembles' by J.-L. Krivine, and often he states "E(x1,...xn)" as a wff where free variables are only among x1,..,xn. Is this notion formalizable in metamath ? It occurs really a lot on all the FOL books i read.
Le lundi 13 janvier 2025 à 17:23:30 UTC, David A. Wheeler a écrit : > > > > 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/dddccc71-655e-4c02-8761-77767a7de681n%40googlegroups.com.
