Printing of multiple optional argument #4812
Comments
kmill
added a commit
to kmill/lean4
that referenced
this issue
Jul 27, 2024
…nting Before, the delaborator was conservative about omitting optional arguments, only omitting the very last one. Now it can omit arbitrarily long sequences of optional arguments from the end. For simplicity of implementation, every optional argument is delaborated and then potentially discarded. It could save state and lazily delaborate, but we're running under the hypothesis that most optional arguments are for very simple values (like `true`, `false`, or a numeric literal), so it is unlikely that efficiency gains, if any, are worth it. In particular, in the future structure constructors will have optional arguments, but `unexpandStructureInstance` assumes none of the optional fields are omitted. Closes leanprover#4812
github-merge-queue bot
pushed a commit
that referenced
this issue
Jul 29, 2024
…nting (#4854) Before, the delaborator was conservative about omitting optional arguments, only omitting the very last one. Now it can omit arbitrarily long sequences of optional arguments from the end. For simplicity of implementation, every optional argument is delaborated and then potentially discarded. It could save state and lazily delaborate, but we're running under the hypothesis that most optional arguments are for very simple values (like `true`, `false`, or a numeric literal), so it is unlikely that efficiency gains, if any, are worth it. In particular, in the future structure constructors will have optional arguments, but `unexpandStructureInstance` assumes none of the optional fields are omitted. Closes #4812
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
A small pretty printer bug in multiple optional argument.
shows
f 0 1 2 : Natinstead off 0 : Natorf 0 1 2 3 : Nat. The last optional argument is missing.Context
Zulip
Discover this bug when using
Array.foldl.Versions
4.9.0
Additional Information
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: