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).
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). 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). Benoît On Friday, June 3, 2022 at 9:47:16 PM UTC+2 Philip White wrote: > This line in the book confuses me: > > > By default Metamath does not show $f hypotheses and everything > > branching off of them in the proof tree when the proof is displayed; > > this makes the proof look more like an ordinary mathematical proof, > > which does not normally incorperate the explicit construction of > > expressions. > > I would expect $f hypotheses to be the leaves of the tree, since it > never takes any extra steps to prove a $f hypothesis. The output of > "show proof some_assertion /all" seems to agree, if I'm interpreting > the indentation correctly as an upside-down tree. > > The context is that I'm working on making the debugger in my UI take > large steps so that you don't have to wade through all the superfluous > steps of a proof. Is understanding this one sentence sufficient to > achieving the same behavior as metamath.exe's "essential" mode view? > > Thanks, > 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/6f075d0b-2a25-42a0-b51f-b1b34bcb001cn%40googlegroups.com.
