mathlib
be93cace - feat(data/list): accessing list with fallback (#15138)

Commit
3 years ago
feat(data/list): accessing list with fallback (#15138) Reimplement `list.inth` in terms of the new `list.nthd`. Implementation wise, it is "faster" because it doesn't have to go through `option.iget` on the way anymore. On the way to computable list-based polynomials
Author
Parents
Loading