Commit 2024-04-04 14:19 e39cbd8f

View on Github →

feat: list lemmas (#11626) Add some general purpose lemmas on lists. The new ext_get?' is intermediate between ext and ext_get, and for consistent naming add an alias ext_get? for ext.

Estimated changes

added theorem List.ext_get?'
added theorem List.ext_get?_iff'
added theorem List.ext_get?_iff
added theorem List.ext_get_iff
added theorem List.head_cons_tail
added theorem List.head_replicate
added theorem List.reverse_concat'
added theorem List.IsPrefix.get_eq
added theorem List.IsPrefix.head_eq
added theorem List.IsPrefix.ne_nil
added theorem List.concat_get_prefix
added theorem List.prefix_concat_iff
added theorem List.prefix_take_iff