collatz/Research/BeattyBlockPotentialBuild.txt at main · Chessing234/collatz · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
⚠ [48/64] Replayed Collatz.Strategy.CycleProduct
warning: Collatz/Strategy/CycleProduct.lean:72:26: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:78:54: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.add_mul, Nat.mul_add, Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:81:54: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.add_mul, Nat.mul_add, Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:86:28: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:158:28: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:197:24: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Collatz/Strategy/CycleProduct.lean:286:24: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [50/64] Replayed Collatz.Strategy.AffineExact
warning: Collatz/Strategy/AffineExact.lean:127:41: Variable name `hm` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hm

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [51/64] Replayed Collatz.Strategy.AccumulatorArith
warning: Collatz/Strategy/AccumulatorArith.lean:129:24: This simp argument is unused:
  Nat.mul_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mul_comm, Nat.mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [63/64] Built Collatz.Strategy.BeattyBlockPotential (30s)
✔ [64/64] Built Collatz.Strategy.BeattyDescentBound (993ms)
Build completed successfully (64 jobs).