Zulip Chat Archive

Stream: general

Topic: funky notation


view this post on Zulip Johan Commelin (Oct 04 2018 at 11:50):

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

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 11:51):

its doomed

view this post on Zulip Johan Commelin (Oct 04 2018 at 11:53):

That's too bad

view this post on Zulip Mario Carneiro (Oct 04 2018 at 14:38):

they are just funny looking brackets...

view this post on Zulip Johan Commelin (Oct 04 2018 at 14:49):

Still it doesn't work )-;

view this post on Zulip Reid Barton (Oct 04 2018 at 14:58):

Shouldn't have the colon after notation

view this post on Zulip Johan Commelin (Oct 04 2018 at 15:01):

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...


Last updated: May 14 2021 at 14:20 UTC