Skip to content

Rework lemmas for `take/drop` of an `++`:

Robbert Krebbers requested to merge robbert/take_drop_app into master
  • Add take_app and drop_app, which are the strongest versions, and use take_app_X for derived versions.
  • Consistently use ' suffix for version with premise n = length, and have versions without ' with length inlined.
  • Rename take_apptake_app_length, take_app_alttake_app_length', take_add_apptake_app_add', take_app3_alttake_app3_length', drop_appdrop_app_length, drop_app_altdrop_app_length', drop_add_appdrop_app_add', drop_app3_altdrop_app3_length'.

This closes #197 (closed).

Merge request reports