Commit 2024-04-02 09:53 ae003d89

View on Github →

feat: findIdx lemmas (#11808) Split from #9781.

Estimated changes

added theorem List.findIdx_eq
added theorem List.findIdx_eq_length
added theorem List.findIdx_le_length
added theorem List.findIdx_lt_length
added theorem List.le_findIdx_of_not
added theorem List.lt_findIdx_of_not
added theorem List.not_of_lt_findIdx