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.
