Skip to content

feat: GenHeap#412

Open
ayhon wants to merge 3 commits into
leanprover-community:masterfrom
ayhon:fele/feat/gen-heap
Open

feat: GenHeap#412
ayhon wants to merge 3 commits into
leanprover-community:masterfrom
ayhon:fele/feat/gen-heap

Conversation

@ayhon
Copy link
Copy Markdown
Contributor

@ayhon ayhon commented May 26, 2026

Description

A GenHeap implementation as a thin wrapper around GhostMap. Since reservation_map is not defined yet, we chose a prior version's gen_heap.v file to port.

Depends on #407, fixes #283.

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have added my name to the authors section of any appropriate files

@ayhon ayhon force-pushed the fele/feat/gen-heap branch from 0deb434 to 510c1e0 Compare May 27, 2026 13:37
@ayhon ayhon force-pushed the fele/feat/gen-heap branch from 6ffad05 to 5fc2ce9 Compare May 29, 2026 11:56
@ayhon ayhon changed the title Fele/feat/gen heap feat: GenHeap May 29, 2026
@ayhon ayhon marked this pull request as ready for review May 29, 2026 12:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Port base_logic/lib/gen_heap.v

1 participant