Skip to content

Rename progress to step #708

@sonmarcho

Description

@sonmarcho

I actually like step better and it is shorter.

In order to make this work properly, the best is to still allow the progress syntax but print a warning suggesting to use the step syntax. Note that the files will need to rename the files (Progress.lean -> Step.lean, etc.)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions