fix: mark ByteArray.Iterator Inhabited instance as noncomputable

[Copilot]

This PR fixes a compiler error where ByteArray.Iterator's derived Inhabited instance conflicts with its custom SizeOf instance that computes size from runtime array values.

Changes

• Removed deriving Inhabited from ByteArray.Iterator structure
• Added explicit noncomputable instance : Inhabited Iterator with documentation explaining the dependency on runtime SizeOf

The custom SizeOf instance computes i.array.size - i.idx, making any Inhabited instance necessarily noncomputable. The previous deriving Inhabited attempted to generate a computable instance, causing the compiler error.

Related: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Compiler.20error.20with.20sizeOf/with/561532734

Original prompt

There is a compiler error reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Compiler.20error.20with.20sizeOf/with/561532734. Reproduce the issue and locate the instance in the lean4 codebase that triggers the error (an instance that uses sizeOf in a way that makes it noncomputable). Modify the instance by marking it noncomputable (use the noncomputable instance declaration form) and add a succinct comment immediately above the instance explaining why it must be noncomputable (e.g. because it depends on sizeOf or runtime information that is not computable). Follow the repository commit conventions for commit message and PR title: use a concise prefix and reference the Zulip discussion URL in the PR body. Include the exact change (file path and contents) in the PR and ensure the repo builds (or at least type checks) after the change. Do not change public API beyond the noncomputable annotation and the comment. Repository: leanprover/lean4

This pull request was created as a result of the following prompt from Copilot chat.

There is a compiler error reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Compiler.20error.20with.20sizeOf/with/561532734. Reproduce the issue and locate the instance in the lean4 codebase that triggers the error (an instance that uses sizeOf in a way that makes it noncomputable). Modify the instance by marking it noncomputable (use the noncomputable instance declaration form) and add a succinct comment immediately above the instance explaining why it must be noncomputable (e.g. because it depends on sizeOf or runtime information that is not computable). Follow the repository commit conventions for commit message and PR title: use a concise prefix and reference the Zulip discussion URL in the PR body. Include the exact change (file path and contents) in the PR and ensure the repo builds (or at least type checks) after the change. Do not change public API beyond the noncomputable annotation and the comment. Repository: leanprover/lean4

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.