From 57c3114875f3fc04a890323353fdd3c44eeaa53d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Apr 2022 15:00:07 -0700 Subject: [PATCH] fix: `simpAll` and tests We need another `update stage0` to remove workaround at `AC.lean` --- src/Init/Data/AC.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 5 +- tests/lean/infoTree.lean.expected.out | 141 ++++++++++---------- tests/lean/simpZetaFalse.lean.expected.out | 2 +- tests/lean/wfrecUnusedLet.lean.expected.out | 2 +- 5 files changed, 76 insertions(+), 76 deletions(-) diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean index 85c96af679..faab678d29 100644 --- a/src/Init/Data/AC.lean +++ b/src/Init/Data/AC.lean @@ -186,7 +186,7 @@ theorem Context.evalList_insert case inr => split case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] - case inr => simp_all [ih, evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] + case inr => simp_all [evalList, EvalInformation.evalOp]; simp [ih]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] -- TODO: remove `simp [ih]` after `update stage0` theorem Context.evalList_sort_congr (ctx : Context α) diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index c8d2c31aab..f835817a69 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -65,8 +65,11 @@ private partial def loop : M Bool := do ``` In the first round, `h : x ≠ 0` is simplified to `h : ¬ x = 0`. If we don't use the same `id`, in the next round the first version would simplify it to `h : True`. + + We must use `mkExpectedTypeHint` because `inferType proofNew` may not be equal to `typeNew` when + we have theorems marked with `rfl`. -/ - let simpThmsNew ← (← getSimpTheorems).addTheorem proofNew (name? := entry.id) + let simpThmsNew ← (← getSimpTheorems).addTheorem (← mkExpectedTypeHint proofNew typeNew) (name? := entry.id) modify fun s => { s with modified := true ctx.simpTheorems := simpThmsNew diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index be4a05fb61..c99ff0b171 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -81,10 +81,7 @@ [.] `x : none @ ⟨17, 43⟩-⟨17, 44⟩ x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ h (isBinder := true) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨17, 4⟩-⟨17, 5⟩ - fun x y b => - of_eq_true - (Eq.trans (congrFun (congrArg Eq (Nat.add_zero x)) x) - (eq_self x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun + fun x y b => of_eq_true (eq_self x) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun Nat : Type @ ⟨18, 6⟩†-⟨18, 7⟩† @ Lean.Elab.Term.elabHole x (isBinder := true) : Nat @ ⟨18, 6⟩-⟨18, 7⟩ Nat : Type @ ⟨18, 8⟩†-⟨18, 9⟩† @ Lean.Elab.Term.elabHole @@ -123,20 +120,20 @@ [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.548} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.544} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.550} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.546} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.553} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.549} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.555} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.551} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ f2 (isBinder := true) : Nat → Nat → Bool → Nat @ ⟨21, 4⟩-⟨21, 6⟩ fun x y b => @@ -193,7 +190,7 @@ ===> Prod.mk✝ (x + y) (x - y) (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp - [.] `Prod.mk._@.infoTree._hyg.90 : some ?_uniq.567 @ ⟨23, 18⟩†-⟨23, 32⟩† + [.] `Prod.mk._@.infoTree._hyg.90 : some ?_uniq.563 @ ⟨23, 18⟩†-⟨23, 32⟩† @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion @@ -231,8 +228,8 @@ [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩ [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩ [.] `Prod.mk._@.infoTree._hyg.104 : some Prod.{0 0} Nat Nat @ ⟨23, 4⟩†-⟨25, 10⟩† - [.] `z : some [mdata _patWithRef: ?_uniq.635] @ ⟨23, 9⟩-⟨23, 10⟩ - [.] `w : some [mdata _patWithRef: ?_uniq.636] @ ⟨23, 12⟩-⟨23, 13⟩ + [.] `z : some [mdata _patWithRef: ?_uniq.631] @ ⟨23, 9⟩-⟨23, 10⟩ + [.] `w : some [mdata _patWithRef: ?_uniq.632] @ ⟨23, 12⟩-⟨23, 13⟩ Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† z (isBinder := true) : Nat @ ⟨23, 9⟩-⟨23, 10⟩ @@ -276,13 +273,13 @@ ===> Prod✝ Nat (Array (Array Nat)) Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Prod._@.infoTree._hyg.129 : some Sort.{?_uniq.761} @ ⟨27, 12⟩†-⟨27, 35⟩† + [.] `Prod._@.infoTree._hyg.129 : some Sort.{?_uniq.757} @ ⟨27, 12⟩†-⟨27, 35⟩† Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.763} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.759} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.762} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.758} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -290,17 +287,17 @@ ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.764} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.760} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.765} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.761} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Sort.{?_uniq.767} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.763} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.768} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.764} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ @@ -313,17 +310,17 @@ [.] Array.getOp s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 8⟩ : some Array.{0} Nat @Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 9⟩-⟨28, 13⟩ s.fst : Nat @ ⟨28, 14⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabProj - [.] `s : some ?_uniq.802 @ ⟨28, 14⟩-⟨28, 15⟩ + [.] `s : some ?_uniq.798 @ ⟨28, 14⟩-⟨28, 15⟩ s : Nat × Array (Array Nat) @ ⟨28, 14⟩-⟨28, 15⟩ @Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.809} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.805} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.811} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.807} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ @@ -340,11 +337,11 @@ f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.831} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.827} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.833} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.829} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ f5 (isBinder := true) : Nat → B @ ⟨33, 4⟩-⟨33, 6⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ @@ -386,86 +383,86 @@ infoTree.lean:44:0: error: expected stx [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩ [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.854} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.850} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.855 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.851 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.856} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.852} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.857 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.855 _uniq.855 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.853 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + Eq.{1} Nat _uniq.851 _uniq.851 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.179 `x `x) - Eq.{1} Nat _uniq.855 _uniq.855 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel + Eq.{1} Nat _uniq.851 _uniq.851 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel [.] `Eq._@.infoTree._hyg.179 : none @ ⟨45, 21⟩†-⟨45, 26⟩† - _uniq.855 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + _uniq.851 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.855 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.855 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + _uniq.851 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ + _uniq.851 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.855 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.861 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ - _uniq.862 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ - _uniq.863 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.862 _uniq.863]) f6.f7 : Eq.{1} Nat _uniq.862 _uniq.862 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec + _uniq.851 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ + _uniq.857 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ + _uniq.858 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.859 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.858 _uniq.859]) f6.f7 : Eq.{1} Nat _uniq.858 _uniq.858 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.864} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.860} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.865 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.861 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.866} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.862} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.867 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.865 _uniq.865 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.863 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.{1} Nat _uniq.861 _uniq.861 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.187 `x `x) - Eq.{1} Nat _uniq.865 _uniq.865 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel + Eq.{1} Nat _uniq.861 _uniq.861 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel [.] `Eq._@.infoTree._hyg.187 : none @ ⟨46, 27⟩†-⟨46, 32⟩† - _uniq.865 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent + _uniq.861 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.865 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.865 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent + _uniq.861 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ + _uniq.861 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.865 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.872 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ - _uniq.873 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ - _uniq.874 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.refl.{1} Nat _uniq.873 : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq.869} Nat _uniq.873 _uniq.873 @ ⟨46, 36⟩-⟨46, 43⟩ + _uniq.861 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ + _uniq.868 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ + _uniq.869 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.870 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.refl.{1} Nat _uniq.869 : Eq.{1} Nat _uniq.869 _uniq.869 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp + [.] `Eq.refl : some Eq.{?_uniq.865} Nat _uniq.869 _uniq.869 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ - _uniq.873 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent - [.] `x : some ?_uniq.876 @ ⟨46, 44⟩-⟨46, 45⟩ - _uniq.873 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ - [mdata _recApp: _uniq.872 _uniq.862 _uniq.863] : Eq.{1} Nat _uniq.862 _uniq.862 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp - [.] `f7 : some Eq.{1} Nat _uniq.862 _uniq.862 @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.872 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.862 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent + _uniq.869 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent + [.] `x : some ?_uniq.872 @ ⟨46, 44⟩-⟨46, 45⟩ + _uniq.869 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ + [mdata _recApp: _uniq.868 _uniq.858 _uniq.859] : Eq.{1} Nat _uniq.858 _uniq.858 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp + [.] `f7 : some Eq.{1} Nat _uniq.858 _uniq.858 @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.868 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.858 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent [.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.862 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent + _uniq.858 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ + _uniq.859 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent [.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩ - _uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ + _uniq.859 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ [Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.896} @ ⟨50, 12⟩-⟨50, 13⟩ + [.] `B : some Sort.{?_uniq.892} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ - _uniq.897 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + _uniq.893 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.898} @ ⟨50, 17⟩-⟨50, 18⟩ + [.] `B : some Sort.{?_uniq.894} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ - _uniq.899 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ - _uniq.900 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ - B.mk (B.pair _uniq.900) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst - B.pair _uniq.900 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj + _uniq.895 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ + _uniq.896 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + B.mk (B.pair _uniq.896) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst + B.pair _uniq.896 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj [.] `b : some Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩ - _uniq.900 : B @ ⟨50, 24⟩-⟨50, 25⟩ - [.] _uniq.900 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A + _uniq.896 : B @ ⟨50, 24⟩-⟨50, 25⟩ + [.] _uniq.896 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩† - pair : Prod.{0 0} A A := B.pair _uniq.900 @ ⟨50, 22⟩†-⟨50, 32⟩ + pair : Prod.{0 0} A A := B.pair _uniq.896 @ ⟨50, 22⟩†-⟨50, 32⟩ f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ diff --git a/tests/lean/simpZetaFalse.lean.expected.out b/tests/lean/simpZetaFalse.lean.expected.out index a2618f4aa9..1d3b02710f 100644 --- a/tests/lean/simpZetaFalse.lean.expected.out +++ b/tests/lean/simpZetaFalse.lean.expected.out @@ -15,7 +15,7 @@ fun x h => (let_congr (Eq.refl (x * x)) fun y => ite_congr (Eq.trans (congrFun (congrArg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a => Eq.refl (y + 1))) 1) - (of_eq_true (Eq.trans (congrFun (congrArg Eq (ite_true 1 (x * x + 1))) 1) (eq_self 1))) + (of_eq_true (eq_self 1)) x z : Nat h : f (f x) = x h' : z = x diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out index 38c47c9012..fdf3093dcf 100644 --- a/tests/lean/wfrecUnusedLet.lean.expected.out +++ b/tests/lean/wfrecUnusedLet.lean.expected.out @@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a => if h : n = 0 then 1 else let y := 42; - 2 * a (n - 1) (_ : (measure id).1 (n - 1) n) + 2 * a (n - 1) (_ : Nat.pred n < n)