Skip to content

Add `last_cons_Some_ne` lemma for the `last` function

Jonas Kastberg requested to merge jihgfee/stdpp:last_lemma into master

A useful lemma for the [last] function, to reduce last (x::l) = Some y to last l = Some y whenever x ≠ y. This is useful since using last_cons leaves us with

match last l with
| Some y0 => Some y0
| None => Some x
end = Some y

which only reduces through a subgoal.

Edited by Robbert Krebbers

Merge request reports