On Fri, Jun 3, 2022 at 7:47 PM 'Philip White' via Metamath < [email protected]> wrote:
> > The divide between ALL and ESSENTIAL is that the latter only shows > > the steps with typecode '|-' (and the final step, whatever its > > typecode is). The other steps, those constructing the formulas and > > classes, are "syntactic", that is, their typecodes are wff, set, > > class (and indeed, their leaves are $f-statements). > > Ohhh, yeah, that makes complete sense. I was expecting that metamath > somehow had an internal concept of what is merely syntactic and what is > essential, but I guess it's just by convention. In other words, if I > were to make a file with different typecodes, then ESSENTIAL mode would > not work so well? (that's easy to verify I guess) > > Probably what I should do is give the user control over the typecodes > they want to consider essential. > One of the things that came out of the research which resulted in the "Models" paper was the "syntax" $j command. In set.mm you can find the following declarations: $( $j syntax 'wff'; syntax '|-' as 'wff'; syntax 'setvar'; syntax 'class'; $) These correspond to the "Syn" function from the paper. In short, there is one of these syntax lines for every legal typecode (that can appear as the initial constant on any $e $f $a $p statement), and the ones that have an 'as' are the logical typecodes (and the thing after the 'as' is the typecode by which to parse the contents) while those that don't have 'as' are grammatical typecodes. So if you wanted to generalize the "is it '|-'?" check, you would instead check if it is a logical typecode. This does require $j parsing however, which is optional for metamath verifiers (since this was intended to be a backward-compatible addition). -- 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/CAFXXJSux%3D4W1pafSBAFYY-rR7TqzveMSySPMs%3DXeU3_omYdRGw%40mail.gmail.com.
