set.mm (in the current folder) is just the default. You can use any .mm file you wish:
- enter VSCode settings ctrl+, - Extensions > Yamma - set 'Mm File Full Path' to your .mm file (mine is set to /mnt/mmt/set.mm ) Glauco p.s. disclaimer: Yamma has mainly been 'tested' on set.mm and subtheories of set.mm Il giorno domenica 30 luglio 2023 alle 23:58:38 UTC+2 [email protected] ha scritto: Are you saying it won't recognize a file not called set.mm? Lamp works on any database, but it doesn't have any option to load a proof from the database. roof from the .mm file? -- 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 on the web visit https://groups.google.com/d/msgid/metamath/84e5364e-bc8a-4a68-b572-a7b43f481c33n%40googlegroups.com.
