`mkValueTypeClosure` type-checks closed terms when the local context has a let
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
This issue has not been assessed yet.
Description
It does this to detect let dependencies, but for closed terms (and even more generally) we can avoid a possibly-expensive check here
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 17m
- Merged PRs (30d)
- 296
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 6 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day