Zulip Chat Archive
Stream: mathlib4
Topic: data.int.succ_pred
Shreyas Srinivas (Jan 13 2023 at 15:19):
Hello everyone,
I see that so far no one has taken up data.int.succ_pred. I will start working on this.
Question : Should the file change to Data.Int.SuccPred (with the underscore removed)?
Chris Hughes (Jan 13 2023 at 15:21):
use scripts/start_port.sh Mathlib/Data/Int/SuccPred.lean to start the port. And read the Porting wiki
Shreyas Srinivas (Jan 13 2023 at 15:38):
Last updated: Dec 20 2023 at 11:08 UTC