-
Notifications
You must be signed in to change notification settings - Fork 251
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
feat: introduce NthRoot
notation class
#7907
base: master
Are you sure you want to change the base?
Conversation
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter. This is extracted from #7907, which adds a more general nth root typeclass. The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot. This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does. While perhaps claiming `√` for `Real.sqrt` is greedy; it: * Is far more common thatn `NNReal.sqrt` and `Nat.sqrt` * Is far more interesting to mathlib than `sqrt` on `Float` * Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types. * Will be replaced by a more general typeclass in a future PR. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
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 pushed some more changes, this now looks great.
@kmill, could you check the unexpander / use of default_instance
is reasonable?
@[app_unexpander NthRoot.nthRoot] | ||
def NthRoot.unexpander : Lean.PrettyPrinter.Unexpander | ||
| `($_ $n $a) => | ||
match n with | ||
| `(2) => `(√$a) | ||
| `(3) => `(∛$a) | ||
| `(4) => `(∜$a) | ||
| _ => `($n:superscript √$a) | ||
| _ => throw () |
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.
If the superscript is complicated (even with just NthRoot.nthRoot (2*n) x
) it won't pretty print correctly. I think restricting to just number literals and identifiers should handle the common cases:
@[app_unexpander NthRoot.nthRoot] | |
def NthRoot.unexpander : Lean.PrettyPrinter.Unexpander | |
| `($_ $n $a) => | |
match n with | |
| `(2) => `(√$a) | |
| `(3) => `(∛$a) | |
| `(4) => `(∜$a) | |
| _ => `($n:superscript √$a) | |
| _ => throw () | |
@[app_unexpander NthRoot.nthRoot] | |
def NthRoot.unexpander : Lean.PrettyPrinter.Unexpander | |
| `($_ 2 $a) => `(√$a) | |
| `($_ 3 $a) => `(∛$a) | |
| `($_ 4 $a) => `(∜$a) | |
| `($_ $n:num $a) | `($_ $n:ident $a) => `($n:superscript √$a) | |
| _ => throw () |
Also use it for
Real.sqrt
, and replace the few occurrences ofsqrt
that do not already use the notation.Zulip