Hi Thierry,
> - "StepName" would be the name of the step, "72" in your example, > - "HypSteps" would be the essential hypotheses, "71,70" in your > example, > - "RefLabel" would be the label of the theorem applied, like "mpbid", > - and "formula" is the formula itself (not shown in your example) > > I've come up with names for the single "components" of the blob, and the formula, but I was looking for a "name" for the whole blob (from the standpoint of my WHITESPACE based tokenizer, it's the first token of a mmp statement, when present; then of course another parser breaks this token down to its components). Are you aware of a formal syntax description of .mmp files? Thanks again Glauco -- 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/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%40googlegroups.com.
