Skip to content

6.1. Messages: swap order of expected error and warning in Docstring #205

@asiz

Description

@asiz

In the last example of this section, the web version of the book shows an error beginning with

❌️ Docstring on #guard_msgs does not match generated message:

This does not appear to be intended, since the problem is just that the Docstring has the error before the warning, but the current version of Lean outputs them in the opposite order. This is since at least August 14th 2025, when I read this part and experimented with an updated version of Lean.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions