Commit 2024-03-26 05:32 7015aaaf

View on Github →

chore(Data/List/GetD): Use Std lemmas (#11653) ... instead of importing Data.Nat.Order.Basic

Estimated changes

modified theorem List.getD_append
modified theorem List.getI_append