> 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. > To see an extreme example, which is kind of abusing the system, see > http://us2.metamath.org/mpeuni/bj-0.html and > http://us2.metamath.org/mpeuni/bj-1.html (see also the head comment > of that section, and compare the results of >show proof xxx/ESSENTIAL > and /ALL on these). Woah, that's real weird. > A clear exposition of the notion of syntactic versus essential (which > extends beyond set.mm) is presented in Mario's article "Models for > Metamath" (the part about weakly grammatical databases, so you do not > have to read through the (harder) part about models). Oh, cool; I'll have to read that. Thanks for the tip. - Philip -- 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/20220603195751.0df48a12%40ithilien.
