Zulip Chat Archive

Stream: mathlib4

Topic: Topology.Basic !4#1826


Yury G. Kudryashov (Jan 25 2023 at 01:31):

I started porting topology.basic in !4#1826, depends on #18288

Yury G. Kudryashov (Jan 25 2023 at 01:47):

Should I use IsOpen or Open?

Jireh Loreaux (Jan 25 2023 at 04:05):

Are we eschewing Is for some reason?

Yury G. Kudryashov (Jan 25 2023 at 04:20):

It seems that compact was renamed to is_compact some time ago, so probably I should use IsOpen.

Frédéric Dupuis (Jan 25 2023 at 05:05):

Is is used all over the place, see for instance docs4#IsSymmOp and friends.

Yury G. Kudryashov (Jan 25 2023 at 05:13):

I remember that there was some discussion about is but I don't remember if it was about adding is or removing is.

Yury G. Kudryashov (Jan 25 2023 at 05:52):

What should I do with the names for docs#Lim, docs#Lim', and docs#lim?

Arien Malec (Jan 25 2023 at 05:53):

I believe the consensus is rename has_foo to Foo but leave is_foo as IsFoo unless there's a compelling reason for alignment to Lean 4 core/std conventions?

This section of the naming wiki is thus far incomplete however.

Arien Malec (Jan 25 2023 at 05:56):

Here's the best consensus on this which amounts to the above:

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ENnReal/near/312549431

Kevin Buzzard (Jan 25 2023 at 08:37):

If we're reopening the is/has debate then I'll say again that is is really really helpful in indicating that the thing you're talking about is a Prop, which is great for teaching.

Yury G. Kudryashov (Jan 25 2023 at 19:53):

Topology.Basic is ready for review.


Last updated: Dec 20 2023 at 11:08 UTC