-
Notifications
You must be signed in to change notification settings - Fork 251
[Add] padRight properties to Data.Vec.Properties #2769
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
Conversation
See also: #2770 . Even if the types of the That being the case, I'll shout out to @JacquesCarette as to whether we go for this PR as is, and refactor downstream, or mark this blocking on #2770 ? UPDATED: see also #2787 |
I should have minded my manners better, and thanked you for the PR before piling in with my nitpicks! These are all, in whatever form they eventually take, a useful contribution... and since |
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.
Hi!
Thanks for your comments! I've made the necessary changes based on your feedback. I just had a small issue with the last point — the irrelevant part of the type signature.
Looking forward to your review of this version!
Great idea for the lemmas for truncate
, will definitely look into that!
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.
More nitpicks, I'm afraid, but otherwise looks good to go...
... but you'll need to write CHANGELOG
entries as well. Suggest you do this once the reset after the v2.3 release is complete, though...
... UPDATED which has now taken place. So, if you look at CHANGELOG.md
, you'll see under Additions to existing modules
... please add the lemma names with their types, and you can see existing versions under eg CHANGELOG/v2.2.md
to see formatting conventions etc.
As I already wrote on #2795 ... UPDATED: I resolved the merge conflicts (which were easy), so I'll re-review, but this looks good now. |
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.
Looks good now
(I'd still change the m
, n
, o
order in padRight-zipWith₁
, but hey...)
…e `truncate-irrelevant`
`fix-whitespace`
This PR adds several equational properties for padRight to Data.Vec.Properties, extending the standard vector operations toolkit with useful lemmas for reasoning about padding on the right.
Added properties:
Each property is proven by structural induction and uses standard lemmas such as
zipWith-replicate, map-replicate, and inject≤.
Authored by : @jmougeot