[Merged by Bors] - feat: Handle powers and multiplicative inverses in cancel_denoms #7819
Conversation
|
Drive-by comment: I think the proper way to format things (so they can be picked up by github) is to make "feat: Handle powers and multiplicative inverses in cancel_denoms" the PR title. The "fixes ..." part should go above the line, so it will become part of the eventual commit message. Thanks for doing this, I'm always excited to see tactic improvements! |
sebzim4500
changed the title
|
This is great -- thanks for the quick fix! bors merge |
github-actions
bot
added
ready-to-merge
fixes #7732 Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
| @@ -177,6 +197,24 @@ partial def mkProdPrf (α : Q(Type u)) (sα : Q(Field $α)) (v : ℕ) (t : Tree | |||
| | t, ~q(-$e) => do | |||
| let v ← mkProdPrf α sα v t e | |||
| mkAppM ``CancelDenoms.neg_subst #[v] | |||
| | .node _ lhs@(.node k1 _ _) (.node k2 .nil .nil), ~q($e1 ^ $e2) => do | |||
There was a problem hiding this comment.
Probably better as
| | .node _ lhs@(.node k1 _ _) (.node k2 .nil .nil), ~q($e1 ^ $e2) => do | |
| | .node _ lhs@(.node k1 _ _) (.node k2 .nil .nil), ~q($e1 ^ ($e2 : ℕ)) => do |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
fixes #7732
Also solves the specific example in #7808, but I would imagine that there are still cases where
cancel_denomsis not idempotent.