WIP: experimenting with HPow as a right action and HSMul as a left action#6852
Closed
WIP: experimenting with HPow as a right action and HSMul as a left action#6852
Conversation
kmill
commented
Aug 30, 2023
kmill
commented
Aug 30, 2023
| open Parser | ||
|
|
||
| /-- Left action; the right argument can participate in the operator coercion elaborator. -/ | ||
| syntax (name := leftact) "leftact% " ident ppSpace term:max ppSpace term:max : term |
Contributor
Author
There was a problem hiding this comment.
This seems to not generate a quot_precheck. If this gets moved to core this shouldn't matter; builtin_term_parser seems to generate one for binop% just fine?
kmill
commented
Aug 30, 2023
|
|
||
| namespace Polynomial | ||
|
|
||
| set_option maxHeartbeats 65000 in |
Contributor
Author
There was a problem hiding this comment.
I think the type ascriptions in this are not actually necessary. My guess is that since binop2.lean is interpreted code instead of compiled code it's consuming a whole lot of heartbeats. The type ascriptions help reduce the number of heartbeats.
kmill
commented
Aug 30, 2023
kmill
commented
Aug 30, 2023
Contributor
|
This just saved me a huge amount of manual type-ascription insertions in porting LeanAPAP. How far are we from merging? |
kmill
added a commit
that referenced
this pull request
Oct 29, 2023
kmill
added a commit
that referenced
this pull request
Nov 9, 2023
Contributor
Author
|
The binop changes were merged into Lean and updated versions of these fixes were merged into master, so closing. |
This was referenced Jan 4, 2024
This was referenced Feb 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is experimenting with some changes to the unary/binary operation elaborator that aim to address lean4#2220
It adds two variants of
binop%:leftact%andrightact%. Whereasbinop%looks at both arguments when doing its coercion computations,leftact%only looks at the right argument andrightact%only looks at the left.Exponentiation is best thought of as being a right action. For example, in
2 ^ n + xwithx : Realandn : Nat, then this should leavenas aNatbut elaborate2as aReal(this is the monoid action ofNatonReal).The main changes to mathlib that are needed are using
(a ^ b :)to essentially switch to thelocal macro_rulessolution for the given expression, using↑(a ^ b)if it's more convenient, or giving type ascriptions to the exponent, like ina ^ (2 : Ordinal).