Commit 2024-11-25 13:34 7113817a

View on Github →

chore: change the definition of List.finRange (#19447) François Dorais has been working on upstreaming List.finRange, but wants to change the definition at the same time. That was running into difficulties, which hopefully are resolved here.

Estimated changes

modified def List.finRange
added theorem List.finRange_eq_nil
added theorem List.finRange_map_get
added theorem List.finRange_zero
added theorem List.getElem_finRange
added theorem List.get_finRange
added theorem List.indexOf_finRange
added theorem List.length_finRange
added theorem List.mem_finRange
added theorem List.nodup_finRange
deleted theorem List.finRange_eq_nil
deleted theorem List.finRange_map_get
deleted theorem List.finRange_zero
deleted theorem List.getElem_finRange
deleted theorem List.get_finRange
deleted theorem List.indexOf_finRange
deleted theorem List.length_finRange
deleted theorem List.mem_finRange
deleted theorem List.nodup_finRange
deleted theorem List.pairwise_le_finRange
deleted theorem List.pairwise_lt_finRange