News for hackers. Stuff that matters.
Re:Lean 4.0.0, first official lean4 release by alimw on Friday September 08, 2023 @08:53AM (#37432858)
Yes split_ifs is in Mathlib so I have replaced it with split (twice) which is in Core. I believe there is also an intermediate level Std. I'm not sure why you'd want to avoid Mathlib but I daresay it's possible for many types of problem.

There are no comments on this comment yet.