Zulip Chat Archive
Stream: mathlib4
Topic: Notation precedence: compl
Yury G. Kudryashov (Jun 29 2023 at 00:31):
What do we need to do with notation for src#HasCompl.compl so that ContinuousOn f {a}ᶜ will parse as ContinuousOn f ({a}ᶜ) instead of (ContinuousOn f {a})ᶜ (here compl stands for not)?
Floris van Doorn (Jun 29 2023 at 13:35):
#5586 (WIP)
Floris van Doorn (Jun 29 2023 at 13:36):
What other notations have wrong precedences / need weird parentheses?
I believe there is something with integrals with bounds?
Yury G. Kudryashov (Jun 29 2023 at 14:04):
For integrals, the plan is to move to ∫_{a}^{b} x, f x
Yury G. Kudryashov (Jun 29 2023 at 14:04):
(at least this is my plan)
Yury G. Kudryashov (Jun 29 2023 at 14:06):
example : 5 = (· + 2)^[2] 1 := rfl -- fails
Yury G. Kudryashov (Jun 29 2023 at 14:25):
Notation for docs#Bundle.TotalSpace.proj needs parentheses in (π E) x
Floris van Doorn (Jun 29 2023 at 15:10):
Floris van Doorn (Jun 29 2023 at 18:38):
Do we want ∫ x, L x ∂μ 37 to mean (∫ x, L x ∂μ) 37? Currently it means ∫ x, L x ∂(μ 37), which seems wrong.
Gabriel Ebner (Jun 29 2023 at 18:41):
Floris van Doorn said:
What other notations have wrong precedences / need weird parentheses?
I'm always surprised that ⨅ i, c = c parses as ⨅ i, (c = c) instead of (⨅ i, c) = c.
Floris van Doorn (Jun 29 2023 at 18:42):
Btw, speedy delegations of #5586, #5589 and #5591 are welcome. I think they're (mostly) good to go.
Yaël Dillies (Jun 29 2023 at 18:50):
The pos_part notation is botched too, although the whole file is botched so maybe let me redo it from scratch.
Scott Morrison (Jun 29 2023 at 23:15):
@Floris van Doorn, #5586 is broken.
Scott Morrison (Jun 29 2023 at 23:18):
I merged #5589.
Yury G. Kudryashov (Jun 29 2023 at 23:48):
Scott Morrison said:
Floris van Doorn, #5586 is broken.
That's why Floris asks for delegation, not merging.
Yury G. Kudryashov (Jun 30 2023 at 00:01):
I resolved a merge conflict in #5586 and fixed errors found by lint (not tested).
Floris van Doorn (Jun 30 2023 at 11:00):
Gabriel Ebner said:
I'm always surprised that
⨅ i, c = cparses as⨅ i, (c = c)instead of(⨅ i, c) = c.
Floris van Doorn (Jun 30 2023 at 11:23):
Yaël Dillies said:
The
pos_partnotation is botched too, although the whole file is botched so maybe let me redo it from scratch.
I need more than that. The occurrences of ⁺ in Algebra/Order/LatticeGroup look fine to me.
Floris van Doorn (Jun 30 2023 at 11:24):
The SetFamily/Shadow file looks bad, I'll fix that notation.
Yaël Dillies (Jun 30 2023 at 11:49):
Yeah sorry, it only came up because I started using pos_part on pi types. f i\pospart currently means (f i)\pospart instead of f (i\pospart).
Floris van Doorn (Jun 30 2023 at 12:03):
oh, that is bad indeed. Does that currently already occur in the library?
Yaël Dillies (Jun 30 2023 at 12:19):
I believe not. pos_part is barely used as of now.
Yury G. Kudryashov (Jun 30 2023 at 12:24):
I wanted to rewrite some proof about integrals in terms of posPart/negPart while porting, then noticed that we have very few lemmas about these functions.
Floris van Doorn (Jun 30 2023 at 12:35):
A few more: #5615 #5618 #5619 #5620
Floris van Doorn (Jun 30 2023 at 12:45):
I want to also fix the precedence of # for cardinal.mk, so that p #α is legal. I think that necessary means that #(α i) requires parentheses.
Eric Rodriguez (Jun 30 2023 at 13:16):
Same as the sqrt thing in the other thread, then
Floris van Doorn (Jun 30 2023 at 14:21):
cardinality precedence is in #5623
Floris van Doorn (Jun 30 2023 at 15:07):
I also fixed the absolute value precedence in #5619, so now you can write max |x| |y| without parentheses.
Yury G. Kudryashov (Jul 02 2023 at 03:11):
In #5660, something is wrong with notation: it fails to parse E ≃ₘ^n[𝕜] E', e.g., on line 132.
Floris van Doorn (Jul 02 2023 at 09:46):
I would appreciate a merge on #5615 and #5619 and a delegation of #5623.
Last updated: Dec 20 2023 at 11:08 UTC