Skip to content

refactor: read back getD/idxOf with Mathlib's getElem?_idxOf - #4849

Merged
SamuelSchlesinger merged 2 commits into
mainfrom
refactor/cx-getd-idxof
Nov 13, 2026
Merged

SamuelSchlesinger merged 2 commits into
mainfrom
refactor/cx-getd-idxof

refactor: migrate the five remaining getD/idxOf read-backs

b6cea80
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
build
succeeded Nov 13, 2026 in 3m 10s