From 92a511be29fe700b2de8602de115b3b7287b8601 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Dec 2021 11:04:40 -0800 Subject: [PATCH] chore: fix test --- tests/lean/infoTree.lean.expected.out | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 860f8b09ec..ead6a3b064 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⟩ @ _aux_Init_Notation___macroRules_«term_×_»_1 + Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1» Macro expansion Nat × Nat ===> @@ -53,13 +53,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⟩ @ _aux_Init_Notation___macroRules_«term_=_»_2 + x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2» 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⟩ @ _aux_Init_Notation___macroRules_«term_+_»_2 + x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion x + 0 ===> @@ -167,7 +167,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⟩ @ _aux_Init_Notation___macroRules_«term_+_»_2 + x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion x + y ===> @@ -177,7 +177,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⟩ @ _aux_Init_Notation___macroRules_«term_-_»_2 + x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ «_aux_Init_Notation___macroRules_term_-__2» Macro expansion x - y ===> @@ -207,7 +207,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⟩ @ _aux_Init_Notation___macroRules_«term_+_»_2 + z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion z + w ===> @@ -218,7 +218,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⟩ @ _aux_Init_Notation___macroRules_«term_+_»_2 + z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion z + z1 ===> @@ -230,7 +230,7 @@ z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ f2 : Nat → Nat → Bool → Nat @ ⟨21, 4⟩-⟨21, 6⟩ [Elab.info] command @ ⟨27, 0⟩-⟨28, 17⟩ @ Lean.Elab.Command.elabDeclaration - Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ _aux_Init_Notation___macroRules_«term_×_»_1 + Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ «_aux_Init_Notation___macroRules_term_×__1» Macro expansion Nat × Array (Array Nat) ===> @@ -345,7 +345,7 @@ infoTree.lean:44:0: error: expected stx [.] `Nat : some Sort.{?_uniq.852} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ _uniq.853 : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.851 _uniq.851 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ _aux_Init_Notation___macroRules_«term_=_»_2 + Eq.{1} Nat _uniq.851 _uniq.851 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> @@ -366,7 +366,7 @@ infoTree.lean:44:0: error: expected stx [.] `Nat : some Sort.{?_uniq.864} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ _uniq.865 : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.863 _uniq.863 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ _aux_Init_Notation___macroRules_«term_=_»_2 + Eq.{1} Nat _uniq.863 _uniq.863 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===>