Commit 2024-03-01 13:29 9a944835

View on Github →

chore(Init/Fin): deprecate Fin.eq_of_veq and Fin.veq_of_eq (#10626) We have Fin.eq_of_val_eq and Fin.val_eq_of_eq in Lean core now. Also slightly shake the tree.

Estimated changes

modified theorem Std.BitVec.ofFin_toFin
modified theorem Finite.of_equiv
modified theorem Fin.eq_of_veq
modified theorem Fin.ne_of_vne
modified theorem Fin.veq_of_eq
modified theorem Fin.vne_of_ne