Update src/Lean/Meta/Constructions/NoConfusion.lean

nomeata · web-flow · commit d643fc902ac6 · 2025-05-22T16:29:57.000+02:00
diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean
@@ -12,7 +12,7 @@ import Lean.Meta.Constructions.NoConfusionLinear
 
 register_builtin_option backwards.linearNoConfusionType : Bool := {
   defValue := true
-  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type, else use for the no-confusion-tyep for inductive types"
+  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. "
 }
 
 namespace Lean

Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,7 @@ import Lean.Meta.Constructions.NoConfusionLinear`
`12`	`12`
`13`	`13`	`register_builtin_option backwards.linearNoConfusionType : Bool := {`
`14`	`14`	`defValue := true`
`15`		- descr := "use the linear-size construction for the `noConfusionType` declaration of an inductive type, else use for the no-confusion-tyep for inductive types"
	`15`	+ 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. "
`16`	`16`	`}`
`17`	`17`
`18`	`18`	`namespace Lean`