Zulip Chat Archive
Stream: general
Topic: Docgen archive
Yaël Dillies (Jun 29 2023 at 20:07):
A funny consequence of including archive in doc-gen is that we now have non-mathlib notations in mathlib docs. Consider docs#real.sqrt (which has no notation defined in mathlib) and https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean#L46
Jireh Loreaux (Jun 29 2023 at 20:59):
That's now docs3#real.sqrt
Yury G. Kudryashov (Jun 30 2023 at 05:20):
BTW, should we use this notation in mathlib?
Eric Rodriguez (Jun 30 2023 at 06:26):
I do really like this notation but precedence may be weird
Eric Rodriguez (Jun 30 2023 at 06:26):
Could we force it to use ()s?
Eric Rodriguez (Jun 30 2023 at 06:27):
Or the latex way, make it take exactly one character
Sebastian Ullrich (Jun 30 2023 at 06:45):
That sounds basically equivalent to giving it max precedence
Yaël Dillies (Jun 30 2023 at 07:32):
Yes, I think it would make sense to add this notation with max precedence to mathlib.
Last updated: Dec 20 2023 at 11:08 UTC