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/20220603155727.39853acc%40ithilien.
