address review

src/Init/Data/BitVec/Basic.lean

@@ -11,10 +11,10 @@ import Init.Data.Int.Bitwise
 import Init.Data.BitVec.BasicAux
 
 /-!
-We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
-(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
-with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
-representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
+others for its relative efficiency (Lean has special support for `Nat`),  and the fact that bitwise
+operations on `Fin` are already defined. Some other possible representations are `List Bool`,
+`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
 
 We define many of the bitvector operations from the
 [`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).

src/Init/Data/BitVec/BasicAux.lean

@@ -8,6 +8,11 @@ import Init.Data.Fin.Basic
 
 set_option linter.missingDocs true
 
+/-!
+This module exists to provide the very basic `BitVec` definitions required for
+`Init.Data.UInt.BasicAux`.
+-/
+
 namespace BitVec
 
 section Nat

src/Init/Data/UInt/BasicAux.lean

@@ -7,6 +7,13 @@ prelude
 import Init.Data.Fin.Basic
 import Init.Data.BitVec.BasicAux
 
+/-!
+This module exists to provide the very basic `UInt8` etc. definitions required for
+`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
+meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
+This file thus breaks the import cycle that would be created by this dependency.
+-/
+
 open Nat
 
 def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin

src/Init/Data/UInt/Lemmas.lean

@@ -45,21 +45,13 @@ theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
 
 @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
 
-protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := by
-  simp only [le_def, lt_def]
-  apply BitVec.le_trans
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
 
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := by
-  simp only [le_def, lt_def]
-  apply BitVec.lt_trans
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
 
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := by
-  simp only [le_def, lt_def]
-  apply BitVec.le_total
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
 
-protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := by
-  simp only [le_def, lt_def]
-  apply BitVec.lt_asymm
+protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
 
 protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl