Zulip Chat Archive

Stream: mathlib4

Topic: notation in TorusIntegral

Kim Morrison (Mar 10 2025 at 08:21):

@Cuma Kökmen / @Yury G. Kudryashov, there is a comment in file#Mathlib/MeasureTheory/Integral/TorusIntegral saying

TODO: restore notation; neg, add etc fail if I use notation here

Could you do one of:

  • work how to fix this and do so,
  • explain what the desired notation actually is
  • or confirm that it's okay to simply delete this porting note

Yury G. Kudryashov (Mar 12 2025 at 03:21):

Let me have a look what it used in mathlib3

Yury G. Kudryashov (Mar 12 2025 at 03:22):

It used superscript n etc.

Yury G. Kudryashov (Mar 12 2025 at 03:23):

I'll have a look now

Yury G. Kudryashov (Mar 12 2025 at 03:40):

The example from the module docstring of @Mario Carneiro 's Util/Superscript doesn't work. I added noWs but I'm getting the following error:

elaboration function for 'term___._@.Mathlib.MeasureTheory.Integral.TorusIntegral._hyg.21' has not been implemented
  ℂⁿ

with this notation:

local syntax:arg term:max noWs superscript(term) : term
local macro_rules | `($a:term noWs $b:superscript) => `(Fin $b → $a)

Yury G. Kudryashov (Mar 12 2025 at 03:40):

What am I doing wrong?

Mario Carneiro (Mar 12 2025 at 03:41):

not sure if this is the issue, but noWs should not be in the match pattern

Yury G. Kudryashov (Mar 12 2025 at 03:42):

Removed, same error.

Mario Carneiro (Mar 12 2025 at 03:42):

have you tried not putting space between them?

Yury G. Kudryashov (Mar 12 2025 at 03:42):

It works! Why?

Mario Carneiro (Mar 12 2025 at 03:43):

well, that's what noWs does :)

Yury G. Kudryashov (Mar 12 2025 at 03:47):

#22864

Yury G. Kudryashov (Mar 12 2025 at 03:48):

Thanks!

Eric Wieser (Mar 12 2025 at 08:56):

I think we concluded that it is not safe to use subscript(term) and subscriptTerm has to be used instead?

Yury G. Kudryashov (Mar 13 2025 at 03:35):

Then the module docstring should be updated.

Yury G. Kudryashov (Mar 13 2025 at 03:36):

(by someone who understand the difference between subscript(term) and subscriptTerm, thus not me)

Mario Carneiro (Mar 13 2025 at 03:37):

that was a workaround for a bug in lean, has it been fixed perhaps?

Eric Wieser (Mar 13 2025 at 10:07):

https://github.com/leanprover/lean4/pull/6325 is still open

Eric Wieser (Mar 13 2025 at 10:08):

Maybe we should just comment out registering the subscript() alias

Last updated: May 02 2025 at 03:31 UTC