Simp.Step.continue vs Simp.DStep.continue

Stream: lean4

[Yaël Dillies]

The docstrings for the constructors of docs#Lean.Meta.Simp.Step and docs#Lean.Meta.Simp.DStep (which is an abbrev for docs#Lean.TransformStep) don't match up: A lot of it is just phrasing or whitespace, but one specific difference caught my attention:

• The docstring for Step.continue says "For post procedures, this is equivalent to returning visit."
• The docstring for DStep.continue says "For post procedures, this is equivalent to returning done."

[Yaël Dillies]

Why is it so? Or is this simply a typo?

[Yaël Dillies]

:ping_pong: It would be great to have an answer since @Paul Lezeau and I are writing two blogposts about simp!

[Yaël Dillies]

@Kyle Miller, as the local simp expert, would you know?

[Kyle Miller]

From reading some of the source code, I got the impression that DStep.continue really is different from Step.continue, but the docstring isn't completely accurate, since there's a difference in DStep and TransformStep even though it's an abbreviation.

It looks like DStep.continue means to continue running the remaining dsimprocs on the same expression. Once there are no more simprocs, then since dsimprocs are run using the Meta.transform framework, the .continue for the last post procedure is the same as .done. (See docs#Lean.Meta.Simp.dandThen for how .continues are composed.)