✔ [2370/2384] Built Omega.Ledger
⚠ [2372/2384] Built Omega.Constants
warning: ././././Omega/Constants.lean:97:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [2373/2384] Built Omega.Affine
warning: ././././Omega/Affine.lean:18:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ././././Omega/Affine.lean:73:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [2374/2384] Built Omega.Floor
warning: ././././Omega/Floor.lean:167:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ././././Omega/Floor.lean:175:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [2375/2384] Built Omega.Interface
✔ [2376/2384] Built Omega.Geometry
✔ [2377/2384] Built Omega.Extinction
⚠ [2378/2384] Built Omega.Metrics
warning: ././././Omega/Metrics.lean:30:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [2379/2384] Built Omega.Placement
⚠ [2380/2384] Built Omega.Dimension
warning: ././././Omega/Dimension.lean:37:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: ././././Omega/Dimension.lean:39:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [2381/2384] Built Omega.Finite
✔ [2382/2384] Built Omega.Main
✔ [2383/2384] Built Omega
Build completed successfully.