Commit 2021-12-21 10:05 70af8b92

View on Github →

chore: snake case tactics (#141) Per the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic.20naming.20convention , tactics should be snake-cased. This implements the mathlib4 part of the conversion, and the mathport part is leanprover-community/mathport#79 .

Estimated changes

modified theorem List.get?_zero
modified def test1
modified def test2
modified def test3
modified def test4
modified def test5
modified def test6