!4#5249 NumberTheory.KummerDedekind

Stream: mathlib4

[Xavier Roblot]

This file defines a local notation

local notation:max R "<" x ">" => adjoin R ({x} : Set S)

However, it does not work:

def conductor (x : S) : Ideal S where
  carrier := {a | ∀ b : S, a * b ∈ R<x>}
...

gives an error at x: expected term. Hovering over the symbols: < is recognised as the first part of the notation, but > is recognised as the strict inequality symbol.

[Damiano Testa]

Does using x:ident in the notation help? Untested, as I am on mobile.

[Sebastian Ullrich]

Use x:max to prevent it from parsing the token as an operator. This of course limits what you can write for x without using parentheses

[Xavier Roblot]

Yes, that works. Thanks!

[Damiano Testa]

Does max mean that the syntax will end as soon as > is found?

[Mario Carneiro]

it means the syntax will end as soon as anything with precedence less than max is found, which basically means only atomic expressions and parentheses-enclosed expressions are allowed

[Mario Carneiro]

a more targeted fix would be to set the precedence one higher than that of >