Commit 2023-06-10 10:48 a55642fc

View on Github →

refactor: Defs and Lemmas files for Bitvec (#4899) The Core file was just dumped from Lean3 core. I've split it into Defs and Lemmas in the style of the List folder for example.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Data/Bitvec/Core.lean to Mathlib/Data/Bitvec/Defs.lean

deleted theorem Bitvec.bitsToNat_toList

deleted theorem Bitvec.bits_toNat_decide

added def Bitvec.ofFin

deleted theorem Bitvec.ofNat_succ

added def Bitvec.toFin

deleted theorem Bitvec.toNat_append

deleted theorem Bitvec.toNat_ofNat

Renamed Mathlib/Data/Bitvec/Basic.lean to Mathlib/Data/Bitvec/Lemmas.lean

added theorem Bitvec.bitsToNat_toList

added theorem Bitvec.bits_toNat_decide

deleted def Bitvec.ofFin

added theorem Bitvec.ofNat_succ

deleted def Bitvec.toFin

added theorem Bitvec.toNat_append

added theorem Bitvec.toNat_ofNat

Modified Mathlib/Data/Num/Bitwise.lean