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

fix: test

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-07-22 17:25:59 -07:00 • committed by Sebastian Ullrich
parent f27a069773
commit 54f2769e13
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3,7 +3,7 @@
[.] `Nat : some Sort.{?_uniq.534} @ ⟨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.2237
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2258
Macro expansion
Nat × Nat
===>
@ -51,13 +51,13 @@
[.] `Bool : some Sort.{?_uniq.572} @ ⟨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.9038
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9563
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.5514
x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.5829
Macro expansion
x + 0
===>
@ -170,7 +170,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.5514
x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.5829
Macro expansion
x + y
===>
@ -180,7 +180,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.5610
x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.5925
Macro expansion
x - y
===>
@ -209,7 +209,7 @@
let z1 : Nat := 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.5514
z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.5829
Macro expansion
z + w
===>
@ -220,7 +220,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.5514
z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.5829
Macro expansion
z + z1
===>
@ -231,7 +231,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.2237
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2258
Macro expansion
Nat × Array (Array Nat)
===>