leanprover / leanprover/lean4

Make use of Top Byte Ignore on AArch64

Open
#2,437 3 comments 0 reactions 1 assignee View on GitHub

@zwarich is already working on this.

Since May 8, 2025.

enhancement low priority P-low
Dominant language
Lean
Stars
9.2k
Forks
990
Avg merge
1d 17h
Merged PRs (30d)
175

Description

Very much a low-priority feature especially as it is platform-dependent, but it would be nice to utilize Top Byte Ignore on supported platforms such that we don't have to shift away the tag of tagged pointers. Might even make sense to move even more information such as the full ctor tag (as done by GHC I believe) into the byte, which may or may not be fruitful for x86 as well.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.