-
Notifications
You must be signed in to change notification settings - Fork 98
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
Achieve parity between Array and List lemmas #24
Comments
A trick I learned from @digama0 is to liberally apply |
There may be other ones, but some of the remaining incongruities between the
It may be helpful to document the difference (if any) between functions like @digama0 if at some point you decide any changes are appropriate, let me know if I can help. |
I am doing some "practical program" proving with lean4, and I have found the following lemma really helpful
If I want to prove some equality of arrays, I use However, it still feels like something is missing, because if I have some I need to manually use this technique on each |
That is |
In order to encourage std4 users to write verifiable code with arrays, we should aim to have a similar set of lemmas for arrays (https://github.com/leanprover/std4/blob/main/Std/Data/Array/Lemmas.lean) as we do for lists (https://github.com/leanprover/std4/blob/main/Std/Data/List/Lemmas.lean).
The text was updated successfully, but these errors were encountered: