funky notation

Stream: general

[Johan Commelin]

Is this doomed to fail?

def is_ideal_adic (J : set A) [is_ideal J] : Prop :=
∀ n, is_open (pow_ideal J n) ∧ (∀ K : set A, (0 : A) ∈ K → is_open K → ∃ n, pow_ideal J n ⊆ K)

notation : `is_`J`_adic` := is_ideal_adic J

[Johannes Hölzl]

its doomed

[Johan Commelin]

That's too bad

[Mario Carneiro]

they are just funny looking brackets...

[Johan Commelin]

Still it doesn't work )-;

[Reid Barton]

Shouldn't have the colon after notation

[Johan Commelin]

Thanks @Reid Barton it works!

notation `is-`J`-adic` := is_ideal_adic J

def is_adic (A₀ : set A) [is_subring A₀] : Prop := ∃ (J : set A₀) [hJ : is_ideal J],
(by haveI := topological_subring A₀; haveI := hJ; exact is-J-adic)

You can't use underscores, or you'll need to leave spaces...