feat: use explicit allowlist instead of transparency bump in whnfMatcher#13363

Merged

nomeata merged 27 commits intomasterfrom

joachim/matchwhnf

Apr 24, 2026

Commits on Apr 10, 2026

refactor: stop bumping transparency to `.instances` in `whnfMatcher`

nomeata
and
claude
committed

Commits on Apr 13, 2026

refactor: use explicit allowlist instead of transparency bump in `whnfMatcher`

nomeata
and
claude
committed
refactor: prune unneeded entries from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: prune more unneeded `canUnfoldAtMatcher` allowlist entries

nomeata
and
claude
committed
refactor: remove Fin.ofNat from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove UInt*.ofNat and UInt*.decEq from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove Nat.sub chain from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove instOfNatNat from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove IntCast.intCast from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove Nat.add chain from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
doc: add comments explaining why each `canUnfoldAtMatcher` entry is needed

nomeata
and
claude
committed
refactor: use `Nat.decEq` instead of `decEq` in derived BEq instances

nomeata
and
claude
committed
refactor: remove Nat.mul chain from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove Pure.pure and Nat.mul chain from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove Least?.least? from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove UpwardEnumerable.succ? from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
refactor: remove GetElem.getElem from `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed
doc: update NatCast.natCast comment in canUnfoldAtMatcher

nomeata
and
claude
committed

Commits on Apr 14, 2026

refactor: add Fin.ofNat to `canUnfoldAtMatcher` allowlist

nomeata
and
claude
committed

Commits on Apr 15, 2026

Commits on Apr 24, 2026