New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(data/seq/seq): prove seq.ext
earlier
#15830
Conversation
This PR/issue depends on:
|
Can you merge master? |
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
exact h.trans (nat.le_succ n) | ||
end⟩ | ||
|
||
instance coe_list : has_coe (list α) (seq α) := ⟨of_list⟩ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IMHO, it is strange to have both a function and a coercion. Which form is the simp
-normal form? I would drop one of them.
OTOH, you don't change the API of |
We heavily golf `seq.ext` and move it to almost the beginning of the file. Doing this breaks the proof of `seq.of_list_cons`, which we also change and golf by adding a few trivial `simp` lemmas (not all of them are needed, but might as well add them).
Pull request successfully merged into master. Build succeeded: |
seq.ext
earlierseq.ext
earlier
We heavily golf
seq.ext
and move it to almost the beginning of the file. Doing this breaks the proof ofseq.of_list_cons
, which we also change and golf by adding a few trivialsimp
lemmas (not all of them are needed, but might as well add them).cons
andtail
def-eqs #15829