Zulip Chat Archive

Stream: maths

Topic: What's with the `_` in `zero_`?


view this post on Zulip Kevin Buzzard (Oct 06 2018 at 23:52):

I've seen this in a few places now:

class is_submodule {α : Type u} {β : Type v} [ring α] [module α β] (p : set β) : Prop :=
(zero_ : (0:β)  p)
(add_  :  {x y}, x  p  y  p  x + y  p)
(smul :  c {x}, x  p  c  x  p)

Why zero_ and add_ but not smul_?

view this post on Zulip Mario Carneiro (Oct 07 2018 at 00:47):

I think we are using ' for this now

view this post on Zulip Mario Carneiro (Oct 07 2018 at 00:47):

it's avoiding a name clash with a restated axiom just below it

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 07:43):

Once we decide on a convention will it mean that a lot of code needs to be rewritten? The idea is that we are separating off the actual constructor (which is supposed to be thought of as hidden?) from the user interface? Of course ' is used in other situations in mathlib to mean something else -- like "oh if you don't want that add_sub_cancel you might instead find add_sub_cancel' useful", right?


Last updated: May 06 2021 at 19:30 UTC