-
Notifications
You must be signed in to change notification settings - Fork 259
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({ Tactic + test }/MoveAdd): make And/Or
left-associative
#8607
Conversation
And/Or
left-associativeAnd/Or
left-associative
| [a] => a | ||
| a::as => | ||
if left_assoc? then | ||
Expr.app (prepOp.app a) (sumList prepOp true as) |
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.
Or alternatively (untested):
Expr.app (prepOp.app a) (sumList prepOp true as) | |
as.foldr (fun x y => Expr.app (prepOp.app x) y) a |
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.
I tried this, but I think that it does not work: the a
should really be the last element of the list. At least, this is what my understanding of foldr
does. So, there may be some more idiomatic way of doing this, but the following would be closer to what it should be:
| l@(a::as) =>
if left_assoc? then
(l.dropLast).foldr (fun x y => Expr.app (prepOp.app x) y) l.getLast!
Thanks, and sorry for the delay! bors merge |
In this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/move_oper.20.20HAnd.2EhAnd.3F/near/403820462) it was pointed out that `move_oper` always assumes right-associativity also for `And/Or`. This PR makes `move_oper` left-associative on `And/Or`. Affected files: ```bash Tactic/MoveAdd test/MoveAdd ```
Build failed (retrying...): |
In this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/move_oper.20.20HAnd.2EhAnd.3F/near/403820462) it was pointed out that `move_oper` always assumes right-associativity also for `And/Or`. This PR makes `move_oper` left-associative on `And/Or`. Affected files: ```bash Tactic/MoveAdd test/MoveAdd ```
Pull request successfully merged into master. Build succeeded: |
And/Or
left-associativeAnd/Or
left-associative
In this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/move_oper.20.20HAnd.2EhAnd.3F/near/403820462) it was pointed out that `move_oper` always assumes right-associativity also for `And/Or`. This PR makes `move_oper` left-associative on `And/Or`. Affected files: ```bash Tactic/MoveAdd test/MoveAdd ```
In this Zulip discussion it was pointed out that
move_oper
always assumes right-associativity also forAnd/Or
.This PR makes
move_oper
left-associative onAnd/Or
.Affected files: