Commit 2024-02-11 03:49 7d2b303e

View on Github →

chore: remove Fintype.card_fin_even (#10273) This instance was meant to apply to even literal numbers. Because Lean 4 no longer uses bit0/bit1 for literals, it no longer serves that purpose. Instead, a specific instance for Fin 2 is added.

Estimated changes