mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
b7ac6243a9
This PR makes it so that in the issue template a line about how to check boxes is in comment form you can only see it when you are creating the issue and it does not need to be displayed to everyone.
1.5 KiB
1.5 KiB
name, about, title, labels, assignees
| name | about | title | labels | assignees |
|---|---|---|---|---|
| Bug report | Create a bug report | bug |
Prerequisites
- Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
- Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)
Description
[Clear and concise description of the issue]
Context
[Broader context that the issue occurred 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 #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]
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.