From 42773941ed5b63ce8f87f94d9282affd428ea004 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Oct 2021 17:00:07 -0700 Subject: [PATCH] chore: fix test --- tests/lean/infoTree.lean.expected.out | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 66d93780d3..049611a242 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -3,7 +3,7 @@ [.] `Nat : some Sort.{?_uniq.405} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x : Nat @ ⟨13, 7⟩-⟨13, 8⟩ - Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2315 + Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2558 Macro expansion Nat × Nat ===> @@ -51,13 +51,13 @@ [.] `Bool : some Sort.{?_uniq.441} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b : Bool @ ⟨17, 23⟩-⟨17, 24⟩ - x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9093 + x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.10072 Macro expansion x + 0 = x ===> binrel% Eq✝ (x + 0)x x + 0 = x : Prop @ ⟨17, 35⟩†-⟨17, 44⟩ @ Lean.Elab.Term.elabBinRel - x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.6125 + x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.6786 Macro expansion x + 0 ===> @@ -164,7 +164,7 @@ Prod.mk✝ (x + y) (x - y) (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† - x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.6125 + x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.6786 Macro expansion x + y ===> @@ -174,7 +174,7 @@ x : Nat @ ⟨23, 19⟩-⟨23, 20⟩ y : Nat @ ⟨23, 23⟩-⟨23, 24⟩ @ Lean.Elab.Term.elabIdent y : Nat @ ⟨23, 23⟩-⟨23, 24⟩ - x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.6221 + x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.6892 Macro expansion x - y ===> @@ -203,7 +203,7 @@ let z1 := z + w; z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl Nat : Type @ ⟨24, 8⟩†-⟨24, 10⟩† @ Lean.Elab.Term.elabHole - z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.6125 + z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.6786 Macro expansion z + w ===> @@ -214,7 +214,7 @@ w : Nat @ ⟨24, 18⟩-⟨24, 19⟩ @ Lean.Elab.Term.elabIdent w : Nat @ ⟨24, 18⟩-⟨24, 19⟩ z1 : Nat @ ⟨24, 8⟩-⟨24, 10⟩ - z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.6125 + z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.6786 Macro expansion z + z1 ===> @@ -225,7 +225,7 @@ z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabIdent z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ [Elab.info] command @ ⟨27, 0⟩-⟨28, 17⟩ @ Lean.Elab.Command.elabDeclaration - Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2315 + Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2558 Macro expansion Nat × Array (Array Nat) ===>