max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-18 11:04:40 -08:00
parent 6499798a35
commit 92a511be29
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
tests/lean/infoTree.lean.expected.out
View file

@ -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)
===>