Commit 2023-01-05 14:40 f0c99391

feat port: Data.List.Basic (#966) cf9386b56953fb40904843af98b7a80757bbe7f9 Notes so far There are various problems with theorems already having been ported. Sometimes there was a change in universe level order, implicit argument order, or explicit arguments order or explicicity of arguments. In these situations I did the following. --Ignore the error and align the old lemma when the difference between the two was just universe. --Align the old lemma with the new lemma but incluce a porting note when the difference was the order of implicit arguments --Make a new lemma with a ' at the end when the difference was to do with explicit arguments. I also added a bunch of definitions that were not imported, possibly with the wrong names. These definitions are repeat, ret, empty, init, last, ilast There is a question to be answered about what to do with list.nth_le, which is discussed on Zulip