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.
[ Parent
| on HN ]
There are no comments on this comment yet.