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

fix: fix test

Browse source
This commit is contained in:
Mario Carneiro 2022-07-31 13:35:12 -04:00 • committed by Leonardo de Moura
parent 89a16daa81
commit 7cefcf1f61
1 changed files with 43 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -408,85 +408,85 @@ infoTree.lean:44:0: error: expected stx
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.1195 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1197 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.1197 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.1195 _uniq.1195 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.1199 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.1197 _uniq.1197 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.182 `x `x)
Eq.{1} Nat _uniq.1195 _uniq.1195 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
Eq.{1} Nat _uniq.1197 _uniq.1197 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.182 : none @ ⟨45, 21⟩†-⟨45, 26⟩†
_uniq.1195 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
_uniq.1197 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1195 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1195 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
_uniq.1197 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1197 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1195 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1201 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.1202 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1203 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1202 _uniq.1203]) f6.f7 : Eq.{1} Nat _uniq.1202 _uniq.1202 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
_uniq.1197 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1203 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.1204 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1205 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1204 _uniq.1205]) f6.f7 : Eq.{1} Nat _uniq.1204 _uniq.1204 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.1205 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1207 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.1207 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.1205 _uniq.1205 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.1209 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.1207 _uniq.1207 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.190 `x `x)
Eq.{1} Nat _uniq.1205 _uniq.1205 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
Eq.{1} Nat _uniq.1207 _uniq.1207 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.190 : none @ ⟨46, 27⟩†-⟨46, 32⟩†
_uniq.1205 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
_uniq.1207 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1205 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1205 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
_uniq.1207 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1207 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1205 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1212 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.1213 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1214 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.1213 : Eq.{1} Nat _uniq.1213 _uniq.1213 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq} Nat _uniq.1213 _uniq.1213 @ ⟨46, 36⟩-⟨46, 43⟩
_uniq.1207 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1214 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.1215 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1216 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.1215 : Eq.{1} Nat _uniq.1215 _uniq.1215 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq} Nat _uniq.1215 _uniq.1215 @ ⟨46, 36⟩-⟨46, 43⟩
Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
_uniq.1213 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
_uniq.1215 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
[.] `x : some ?_uniq @ ⟨46, 44⟩-⟨46, 45⟩
_uniq.1213 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.1212 _uniq.1202 _uniq.1203] : Eq.{1} Nat _uniq.1202 _uniq.1202 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
[.] `f7 : some Eq.{1} Nat _uniq.1202 _uniq.1202 @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1212 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1202 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
_uniq.1215 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.1214 _uniq.1204 _uniq.1205] : Eq.{1} Nat _uniq.1204 _uniq.1204 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
[.] `f7 : some Eq.{1} Nat _uniq.1204 _uniq.1204 @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1214 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1204 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
[.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1202 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1203 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
_uniq.1204 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1205 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
[.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩
_uniq.1203 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
_uniq.1205 : 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} @ ⟨50, 12⟩-⟨50, 13⟩
B : Type @ ⟨50, 12⟩-⟨50, 13⟩
_uniq.1239 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
_uniq.1241 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq} @ ⟨50, 17⟩-⟨50, 18⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩
_uniq.1241 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.1242 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.1242) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
_uniq.1242 : B @ ⟨50, 24⟩-⟨50, 25⟩
B.pair _uniq.1242 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
_uniq.1243 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.1244 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.1244) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
_uniq.1244 : B @ ⟨50, 24⟩-⟨50, 25⟩
B.pair _uniq.1244 : 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.1242 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.1242 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
_uniq.1244 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.1244 : 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.1242 @ ⟨50, 22⟩†-⟨50, 32⟩
pair : Prod.{0 0} A A := B.pair _uniq.1244 @ ⟨50, 22⟩†-⟨50, 32⟩
f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩