There's no reason there can't be more than one logical typecode. E.g., in iset.mm, one might add a new typecode |= for classical theorems, with axioms making |= ph equivalent to |- -. -. ph. It mainly isn't done because it would require every theorem to be written multiple times with the different typecodes. For grammar checking, you'd just want to make sure to add a $( $j syntax '|=' as 'wff'; $) comment, as described in the Metamath $j commands <https://us.metamath.org/mpeuni/mm-j-commands.html> page.
Matthew House On Thu, Sep 11, 2025 at 2:29 PM Marlo Bruder <[email protected]> wrote: > Hello everyone, > > I'm currently trying to understant what exactly makes a metamath database > "grammatical" and I have run into a question I wanted to ask: Is it > possible for a grammatical database to have more than one logical typecode? > So far I've only seen databases with one logical typecode (usually ' |- '), > but I don't really see a reason why this shouldn't be possible. > > Much thanks for any answer in advance! > > Best regards, > Marlo Bruder > > -- > 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/4a02c164-1ba7-4356-8e9c-1f0fd9205aa2n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4a02c164-1ba7-4356-8e9c-1f0fd9205aa2n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CADBQv9Z4Yv8PkNv%3Do0ot5S%2BTwKSFWRTksu%2BziSYND%3DPgOvjFYw%40mail.gmail.com.
