Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 03:24 be93cace

View on Github →

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

Estimated changes

added theorem primrec.list_nthd
added theorem list.inth_append
added theorem list.inth_append_right
added theorem list.inth_cons_succ
added theorem list.inth_cons_zero
added theorem list.inth_eq_default
added theorem list.inth_eq_iget_nth
added theorem list.inth_eq_nth_le
added theorem list.inth_nil
added theorem list.nthd_append
added theorem list.nthd_append_right
added theorem list.nthd_cons_succ
added theorem list.nthd_cons_zero
added theorem list.nthd_eq_default
added theorem list.nthd_eq_nth_le
added theorem list.nthd_nil
modified def list.inth
added def list.nthd