Skip to content

Commit 3864be5

Browse files
RaggedRclaude
andcommitted
fix: Mathlib.lean ordering + longFile option for ClayworthSurface
- Move CellularSurface before Colex in Mathlib.lean (alphabetical) - Add set_option linter.style.longFile 4200 for the 4048-line Clayworth surface data file (genus 505, 4032 vertices) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 7e13510 commit 3864be5

2 files changed

Lines changed: 2 additions & 1 deletion

File tree

Archive/ClayworthSurface.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ rather than `![...]` vectors (nested `Fin.cons`, O(n) elaboration).
3131
A helper converts `Array` + size proof → `Fin n → α`.
3232
-/
3333

34+
set_option linter.style.longFile 4200
3435
set_option linter.style.nativeDecide false
3536

3637
/-- Convert an Array to a function on Fin, given a proof that the array has

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3491,9 +3491,9 @@ public import Mathlib.Combinatorics.Additive.RuzsaCovering
34913491
public import Mathlib.Combinatorics.Additive.SmallTripling
34923492
public import Mathlib.Combinatorics.Additive.SubsetSum
34933493
public import Mathlib.Combinatorics.Additive.VerySmallDoubling
3494+
public import Mathlib.Combinatorics.CellularSurface
34943495
public import Mathlib.Combinatorics.Colex
34953496
public import Mathlib.Combinatorics.Compactness
3496-
public import Mathlib.Combinatorics.CellularSurface
34973497
public import Mathlib.Combinatorics.Configuration
34983498
public import Mathlib.Combinatorics.Derangements.Basic
34993499
public import Mathlib.Combinatorics.Derangements.Exponential

0 commit comments

Comments
 (0)