Skip to content

Commit 1c5de37

Browse files
kim-emclaude
andcommitted
fix: drop stale Reorder defs re-added during merge
`Reorder.permuteUniv` and `Reorder.isEmpty` (on the pre-leanprover-community#36604 shape of `Reorder`) were deleted by leanprover-community#36604 when the structure was renamed to `ArgReorder` and a new `Reorder` wrapper was introduced. They were accidentally re-added during a merge resolution and reference a `Reorder` type that is not yet in scope at that point. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent c11913a commit 1c5de37

1 file changed

Lines changed: 0 additions & 13 deletions

File tree

Mathlib/Tactic/Translate/Reorder.lean

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -59,19 +59,6 @@ open Lean Meta Elab
5959
/-- A permutation, represented using cycle notation. -/
6060
abbrev Permutation := List {l : List Nat // 2 ≤ l.length}
6161

62-
/-- Permute a list of either universe levels or universe parameters.
63-
The current heuristic is to swap the first two universes if the first argument is permuted. -/
64-
def Reorder.permuteUniv {α} (r : Reorder) (us : List α) : List α :=
65-
if r.perm.any (·.1.contains 0) then
66-
if let x :: y :: l := us then
67-
y :: x :: l
68-
else us
69-
else us
70-
71-
/-- Return `true` if the reorder doesn't do anything. -/
72-
def Reorder.isEmpty : Reorder → Bool
73-
| { perm, argReorders } => perm.isEmpty && argReorders.isEmpty
74-
7562
namespace Permutation
7663

7764
/-- Permute an array of arguments using the given reorder. -/

0 commit comments

Comments
 (0)