From cce4873c25588cc403d6271d559ac0804abb7426 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 21 Nov 2025 11:57:56 +0100 Subject: [PATCH] chore: rename wrongly named `backwards.` options to `backward.` (#11303) This PR renames rename wrongly named `backwards.` options to `backward.` --- src/Lean/Meta/Constructions/NoConfusion.lean | 6 +++--- src/Lean/Meta/Match/Match.lean | 8 ++++---- tests/lean/run/issue10749.lean | 2 +- tests/lean/run/match1.lean | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean index 02c2583ab3..9f4b2868b1 100644 --- a/src/Lean/Meta/Constructions/NoConfusion.lean +++ b/src/Lean/Meta/Constructions/NoConfusion.lean @@ -45,7 +45,7 @@ def mkNoConfusionCtorArg (ctorName : Name) (P : Expr) : MetaM Expr := do t := mkForall name .default eq t mkLambdaFVars (xs ++ fields1 ++ fields2) t -register_builtin_option backwards.linearNoConfusionType : Bool := { +register_builtin_option backward.linearNoConfusionType : Bool := { defValue := true descr := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. " } @@ -54,7 +54,7 @@ def mkNoConfusionTypeName (indName : Name) : Name := Name.str indName "noConfusionType" def canUseLinear (indName : Name) : MetaM Bool := do - unless backwards.linearNoConfusionType.get (← getOptions) do return false + unless backward.linearNoConfusionType.get (← getOptions) do return false -- Check if the prelude is loaded unless (← hasConst ``Eq.propIntro) do return false -- Check if we have the constructor elim helpers @@ -74,7 +74,7 @@ def mkNoConfusionType (indName : Name) : MetaM Unit := do let ConstantInfo.inductInfo info ← getConstInfo indName | unreachable! let useLinearConstruction := (info.numCtors > 2) && - backwards.linearNoConfusionType.get (← getOptions) && + backward.linearNoConfusionType.get (← getOptions) && (← hasConst (mkCtorElimName indName)) let casesOnName := mkCasesOnName indName let casesOnInfo ← getConstVal casesOnName diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 03c6e24f29..d29827c0d5 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -18,7 +18,7 @@ public section namespace Lean.Meta.Match -register_builtin_option backwards.match.sparseCases : Bool := { +register_builtin_option backward.match.sparseCases : Bool := { defValue := true descr := "if true (the default), generate and use sparse case constructs when splitting inductive types. In some cases this will prevent Lean from noticing that a match statement is complete @@ -27,7 +27,7 @@ register_builtin_option backwards.match.sparseCases : Bool := { ," } -register_builtin_option backwards.match.rowMajor : Bool := { +register_builtin_option backward.match.rowMajor : Bool := { defValue := true descr := "If true (the default), match compilation will split the discrimnants based \ on position of the first constructor pattern in the first alternative. If false, \ @@ -580,7 +580,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do -- We use a sparse case analysis only if there is at least one non-constructor pattern, -- but not just because there are constructors missing (in that case we benefit from -- the eager split in ruling out constructors by type or by a more explicit error message) - if backwards.match.sparseCases.get (← getOptions) && hasVarOrInaccessiblePattern p then + if backward.match.sparseCases.get (← getOptions) && hasVarOrInaccessiblePattern p then let ctors := collectCtors p trace[Meta.Match.match] "using sparse cases: {ctors}" pure (some ctors) @@ -918,7 +918,7 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do process p return - if backwards.match.rowMajor.get (← getOptions) then + if backward.match.rowMajor.get (← getOptions) then match firstRefutablePattern p with | some i => if i > 0 then diff --git a/tests/lean/run/issue10749.lean b/tests/lean/run/issue10749.lean index 2fa2802148..e46e610e40 100644 --- a/tests/lean/run/issue10749.lean +++ b/tests/lean/run/issue10749.lean @@ -121,7 +121,7 @@ fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 => -- Just testing the backwards compatibility option set_option match.ignoreUnusedAlts true in -set_option backwards.match.rowMajor false in +set_option backward.match.rowMajor false in def testOld (a : List Nat) : Nat := match a with | _ => 3 diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean index 245d394766..736a31197a 100644 --- a/tests/lean/run/match1.lean +++ b/tests/lean/run/match1.lean @@ -143,7 +143,7 @@ match n, parity n with | _, Parity.even j => false :: natToBin j | _, Parity.odd j => true :: natToBin j -set_option backwards.match.sparseCases false in +set_option backward.match.sparseCases false in /-- error: Tactic `cases` failed with a nested error: Dependent elimination failed: Failed to solve equation