diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 685fc63c01..8e402c3319 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -520,8 +520,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do mkInductiveDecl vars views mkSizeOfInstances view0.declName Lean.Meta.IndPredBelow.mkBelow view0.declName - -- for view in views do - -- mkInjectiveTheorems view.declName + for view in views do + mkInjectiveTheorems view.declName applyDerivingHandlers views end Lean.Elab.Command diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index a954c987c2..15e09dbbb1 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -582,7 +582,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := } unless isClass do mkSizeOfInstances declName - -- mkInjectiveTheorems declName + mkInjectiveTheorems declName return declName derivingClassViews.forM fun view => view.applyHandlers #[declName] diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index f20538dcdf..a6e74dee5d 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -1,6 +1,6 @@ [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ - [.] `Nat : some Sort.{?_uniq.237} @ ⟨13, 11⟩-⟨13, 14⟩ + [.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x : Nat @ ⟨13, 7⟩-⟨13, 8⟩ Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @@ -10,10 +10,10 @@ Prod✝ Nat Nat Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 22⟩† Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ - [.] `Nat : some Type.{?_uniq.241} @ ⟨13, 18⟩-⟨13, 21⟩ + [.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ - [.] `Nat : some Type.{?_uniq.240} @ ⟨13, 24⟩-⟨13, 27⟩ + [.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ let y : Nat × Nat := (x, x); id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @@ -38,16 +38,16 @@ [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ - [.] `Nat : some Sort.{?_uniq.270} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ x : Nat @ ⟨17, 9⟩-⟨17, 10⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ - [.] `Nat : some Sort.{?_uniq.272} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.570} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ y : Nat @ ⟨17, 11⟩-⟨17, 12⟩ Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ - [.] `Bool : some Sort.{?_uniq.275} @ ⟨17, 27⟩-⟨17, 31⟩ + [.] `Bool : some Sort.{?_uniq.573} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b : Bool @ ⟨17, 23⟩-⟨17, 24⟩ x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @@ -112,20 +112,20 @@ [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ - [.] `Nat : some Sort.{?_uniq.592} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.890} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ - [.] `Nat : some Sort.{?_uniq.594} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.892} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ - [.] `Bool : some Sort.{?_uniq.597} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.895} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ - [.] `Nat : some Sort.{?_uniq.599} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.897} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ fun (x y : Nat) (b : Bool) => let x : Nat × Nat := (x + y, x - y); @@ -230,27 +230,27 @@ Prod✝ Nat (Array (Array Nat)) Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 16⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ - [.] `Nat : some Type.{?_uniq.1602} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.1900} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ - [.] `Array : some Type.{?_uniq.1601} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.1899} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ Macro expansion (Array Nat) ===> Array Nat - [.] `Array : some Type.{?_uniq.1603} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.1901} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ - [.] `Nat : some Type.{?_uniq.1604} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.1902} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ - [.] `Array : some Sort.{?_uniq.1606} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.1904} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ - [.] `Nat : some Type.{?_uniq.1607} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.1905} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ @@ -264,11 +264,11 @@ Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ - [.] `B : some Sort.{?_uniq.1648} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.1946} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ - [.] `Nat : some Sort.{?_uniq.1650} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.1948} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ arg : B @ ⟨31, 2⟩-⟨31, 5⟩ @@ -281,11 +281,11 @@ 0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ - [.] `Nat : some Sort.{?_uniq.1670} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.1968} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ - [.] `B : some Sort.{?_uniq.1672} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.1970} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩