leanprover/lean4

`

Closed this issue · 1 comments

fpfu commented

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

[Clear and concise description of the issue]

Context

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

Expected behavior: [Clear and concise description of what you expect to happen]

Actual behavior: [Clear and concise description of what actually happens]

Versions

[Output of #eval Lean.versionString or of lean --version in the folder that the issue occured in]
[OS version]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

This looks like an accident. I’ll close this one, open a new issue if you want to try again.