Commit 2023-01-07 10:11 95c0d9aa

View on Github →

chore: remove @[simp] from headI (#1407)

Estimated changes

Modified Mathlib/Init/Data/List/Basic.lean

modified def List.headI

added theorem List.headI_cons

added theorem List.headI_nil