Zulip Chat Archive

Stream: mathlib4

Topic: referring to namespace in theorem name


Patrick Massot (Dec 13 2022 at 16:09):

I have a theorem about Sigma.mk, docs#set.range_sigma_mk. What should be the Lean 4 name: Set.range_sigma_mk or Set.range_sigmaMk or something else?

Floris van Doorn (Dec 13 2022 at 16:12):

I think we should refer to Foo.bar and Foo.Bar inside lemmas as fooBar (or bar if the namespace is not necessary to include). So I think it should be Set.range_sigmaMk.

Floris van Doorn (Dec 13 2022 at 16:13):

I came across the same issue in Data.Nat.Cast.Basic with lemmas like theorem op_natCast (n : ℕ) : op (n : α) = n, which seems better to me than op_nat_cast.


Last updated: Dec 20 2023 at 11:08 UTC