Zulip Chat Archive

Stream: mathlib4

Topic: Nat.repeat vs Nat.iterate

Yuyang Zhao (Jul 09 2023 at 12:49):

Why do we have both docs#Nat.repeat and docs#Nat.iterate ?

Eric Wieser (Jul 09 2023 at 12:53):

It looks like Mathlib/Init/Data/Nat/Lemmas.lean is an ad-hoc port, which is probably why it has left this mess behind

Ruben Van de Velde (Jul 09 2023 at 12:53):

No, we already had both in lean 3 core

Ruben Van de Velde (Jul 09 2023 at 12:55):

Oh, but docs3#nat.repeat and docs#Nat.repeat don't match

Ruben Van de Velde (Jul 09 2023 at 12:58):

The new repeat was probably added with no concern for what existed in mathlib 3. Maybe it's worth filling an issue about

Eric Wieser (Jul 09 2023 at 14:02):

Eric Wieser said:

It looks like Mathlib/Init/Data/Nat/Lemmas.lean is an ad-hoc port

I've started a re-port at #5782

Eric Wieser (Jul 09 2023 at 16:51):

This now gives a panic‽

Last updated: Dec 20 2023 at 11:08 UTC