From 122748ab0613e1990ff15637f5ed7310a2879151 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 19 Jul 2022 12:32:18 -0400 Subject: [PATCH] test: strip some more indices --- tests/common.sh | 2 +- .../1018unknowMVarIssue.lean.expected.out | 16 ++-- .../lean/forallMetaBounded.lean.expected.out | 2 +- tests/lean/infoTree.lean.expected.out | 87 +++++++++---------- 4 files changed, 51 insertions(+), 56 deletions(-) diff --git a/tests/common.sh b/tests/common.sh index 990ac52bf3..698faddae0 100644 --- a/tests/common.sh +++ b/tests/common.sh @@ -28,7 +28,7 @@ function compile_lean { function exec_capture { # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them # also strip intermittent "building '/nix/store/..." messages - LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out" + LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out" } # Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise. diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index 811bd2b600..63a7d8e10d 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -9,15 +9,15 @@ a : α ⊢ α [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `α : some Sort.{?_uniq.311} @ ⟨7, 13⟩-⟨7, 14⟩ + [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `α : some Sort.{?_uniq.317} @ ⟨7, 13⟩-⟨7, 14⟩ + [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩ α : Type @ ⟨7, 13⟩-⟨7, 14⟩ a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp - [.] `Fam2 : some Sort.{?_uniq.319} @ ⟨7, 21⟩-⟨7, 25⟩ + [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩ Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩ @@ -27,7 +27,7 @@ a : α β : Type @ ⟨7, 28⟩-⟨7, 29⟩ x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `β : some Sort.{?_uniq.321} @ ⟨7, 33⟩-⟨7, 34⟩ + [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩ β : Type @ ⟨7, 33⟩-⟨7, 34⟩ _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩† a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ @@ -45,8 +45,8 @@ a : α [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.656]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.657]]]) @ ⟨9, 4⟩-⟨9, 12⟩ - [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.656]]] @ ⟨8, 2⟩†-⟨10, 19⟩† + [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩ + [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩† α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩† @@ -57,9 +57,9 @@ a : α Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩ [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.688]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.689]]]) @ ⟨10, 4⟩-⟨10, 12⟩ + [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩ [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩ - [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.688]]] @ ⟨8, 2⟩†-⟨10, 19⟩† + [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ diff --git a/tests/lean/forallMetaBounded.lean.expected.out b/tests/lean/forallMetaBounded.lean.expected.out index 5e9817c51b..5ce01b62f3 100644 --- a/tests/lean/forallMetaBounded.lean.expected.out +++ b/tests/lean/forallMetaBounded.lean.expected.out @@ -1 +1 @@ -Set ?_uniq.1 +Set ?_uniq diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index dfb81f08dd..a0b68cb6e0 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -2,7 +2,7 @@ [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨11, 0⟩-⟨11, 26⟩ [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.397} @ ⟨13, 11⟩-⟨13, 14⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩ Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1» @@ -11,13 +11,13 @@ ===> Prod✝ Nat Nat Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp - [.] `Prod._@.infoTree._hyg.35 : some Sort.{?_uniq.399} @ ⟨13, 18⟩†-⟨13, 27⟩† + [.] `Prod._@.infoTree._hyg.35 : some Sort.{?_uniq} @ ⟨13, 18⟩†-⟨13, 27⟩† Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩† Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.401} @ ⟨13, 18⟩-⟨13, 21⟩ + [.] `Nat : some Type.{?_uniq} @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.400} @ ⟨13, 24⟩-⟨13, 27⟩ + [.] `Nat : some Type.{?_uniq} @ ⟨13, 24⟩-⟨13, 27⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ f (isBinder := true) : Nat → Nat × Nat @ ⟨13, 4⟩-⟨13, 5⟩ x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩ @@ -33,34 +33,32 @@ [.] `Prod.mk._@._internal._hyg.0 : some Prod.{0 0} Nat Nat @ ⟨14, 11⟩†-⟨14, 17⟩† @Prod.mk : {α β : Type} → α → β → α × β @ ⟨14, 11⟩†-⟨14, 17⟩† x : Nat @ ⟨14, 12⟩-⟨14, 13⟩ @ Lean.Elab.Term.elabIdent - [.] `x : some ?_uniq.418 @ ⟨14, 12⟩-⟨14, 13⟩ + [.] `x : some ?_uniq @ ⟨14, 12⟩-⟨14, 13⟩ x : Nat @ ⟨14, 12⟩-⟨14, 13⟩ x : Nat @ ⟨14, 15⟩-⟨14, 16⟩ @ Lean.Elab.Term.elabIdent - [.] `x : some ?_uniq.419 @ ⟨14, 15⟩-⟨14, 16⟩ + [.] `x : some ?_uniq @ ⟨14, 15⟩-⟨14, 16⟩ x : Nat @ ⟨14, 15⟩-⟨14, 16⟩ y (isBinder := true) : Nat × Nat @ ⟨14, 6⟩-⟨14, 7⟩ id y : Nat × Nat @ ⟨15, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabApp [.] `id : some Prod.{0 0} Nat Nat @ ⟨15, 2⟩-⟨15, 4⟩ @id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩ y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabIdent - [.] `y : some ?_uniq.409 @ ⟨15, 5⟩-⟨15, 6⟩ + [.] `y : some ?_uniq @ ⟨15, 5⟩-⟨15, 6⟩ y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩ f (isBinder := true) : Nat → Nat × Nat @ ⟨13, 4⟩-⟨13, 5⟩ -infoTree.lean:18:10: warning: unused variable `b` -infoTree.lean:18:8: warning: unused variable `y` [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.429} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ x (isBinder := true) : Nat @ ⟨17, 9⟩-⟨17, 10⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.431} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ y (isBinder := true) : Nat @ ⟨17, 11⟩-⟨17, 12⟩ Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.434} @ ⟨17, 27⟩-⟨17, 31⟩ + [.] `Bool : some Sort.{?_uniq} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b (isBinder := true) : Bool @ ⟨17, 23⟩-⟨17, 24⟩ x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2» @@ -115,24 +113,23 @@ infoTree.lean:18:8: warning: unused variable `y` ⊢ x + 0 = x after no goals h (isBinder := true) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨17, 4⟩-⟨17, 5⟩ -infoTree.lean:22:10: warning: unused variable `b` [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.562} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.564} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.567} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.569} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ f2 (isBinder := true) : Nat → Nat → Bool → Nat @ ⟨21, 4⟩-⟨21, 6⟩ fun x y b => @@ -189,7 +186,7 @@ infoTree.lean:22:10: warning: unused variable `b` ===> Prod.mk✝ (x + y) (x - y) (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp - [.] `Prod.mk._@.infoTree._hyg.88 : some ?_uniq.581 @ ⟨23, 18⟩†-⟨23, 32⟩† + [.] `Prod.mk._@.infoTree._hyg.88 : some ?_uniq @ ⟨23, 18⟩†-⟨23, 32⟩† @Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ «_aux_Init_Notation___macroRules_term_+__2» Macro expansion @@ -223,12 +220,12 @@ infoTree.lean:22:10: warning: unused variable `b` let z1 := z + w; z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabMatch [.] `Prod.mk._@.infoTree._hyg.102 : none @ ⟨23, 4⟩†-⟨25, 10⟩† - @Prod.mk : {α : Type ?u.662} → {β : Type ?u.661} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† + @Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩† [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩ [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩ [.] `Prod.mk._@.infoTree._hyg.102 : some Prod.{0 0} Nat Nat @ ⟨23, 4⟩†-⟨25, 10⟩† - [.] `z : some [mdata _patWithRef: ?_uniq.675] @ ⟨23, 9⟩-⟨23, 10⟩ - [.] `w : some [mdata _patWithRef: ?_uniq.676] @ ⟨23, 12⟩-⟨23, 13⟩ + [.] `z : some [mdata _patWithRef: ?_uniq] @ ⟨23, 9⟩-⟨23, 10⟩ + [.] `w : some [mdata _patWithRef: ?_uniq] @ ⟨23, 12⟩-⟨23, 13⟩ (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @@ -272,13 +269,13 @@ infoTree.lean:22:10: warning: unused variable `b` ===> Prod✝ Nat (Array (Array Nat)) Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Prod._@.infoTree._hyg.127 : some Sort.{?_uniq.809} @ ⟨27, 12⟩†-⟨27, 35⟩† + [.] `Prod._@.infoTree._hyg.127 : some Sort.{?_uniq} @ ⟨27, 12⟩†-⟨27, 35⟩† Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.811} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.810} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -286,17 +283,17 @@ infoTree.lean:22:10: warning: unused variable `b` ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.812} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.813} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Sort.{?_uniq.815} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.816} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ @@ -314,24 +311,24 @@ infoTree.lean:22:10: warning: unused variable `b` [inst : Inhabited Elem] → (xs : Cont) → (i : Idx) → [inst : Decidable (Dom xs i)] → Elem @ ⟨28, 2⟩†-⟨28, 9⟩† s.snd : Array (Array Nat) @ ⟨28, 2⟩-⟨28, 5⟩ @ Lean.Elab.Term.elabProj - [.] `s : some ?_uniq.822 @ ⟨28, 2⟩-⟨28, 3⟩ + [.] `s : some ?_uniq @ ⟨28, 2⟩-⟨28, 3⟩ s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ @Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩ 1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩ @ Lean.Elab.Term.elabNumLit [.] s.snd[1]! : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ : some Array.{0} Nat @Array.push : {α : Type} → Array α → α → Array α @ ⟨28, 10⟩-⟨28, 14⟩ s.fst : Nat @ ⟨28, 15⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabProj - [.] `s : some ?_uniq.1120 @ ⟨28, 15⟩-⟨28, 16⟩ + [.] `s : some ?_uniq @ ⟨28, 15⟩-⟨28, 16⟩ s : Nat × Array (Array Nat) @ ⟨28, 15⟩-⟨28, 16⟩ @Prod.fst : {α β : Type} → α × β → α @ ⟨28, 17⟩-⟨28, 18⟩ f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1132} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1134} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ @@ -346,14 +343,13 @@ infoTree.lean:22:10: warning: unused variable `b` A.val : A → Nat → Nat @ ⟨31, 15⟩-⟨31, 18⟩ 0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ -infoTree.lean:33:8: warning: unused variable `x` [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1154} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1156} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ f5 (isBinder := true) : Nat → B @ ⟨33, 4⟩-⟨33, 6⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ @@ -394,10 +390,10 @@ bitwise bne infoTree.lean:41:0: error: expected identifier or term [Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ Lean.Elab.Command.elabDeclaration Inhabited Nat : Type @ ⟨39, 11⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabApp - [.] `Inhabited : some Sort.{?_uniq.1177} @ ⟨39, 11⟩-⟨39, 20⟩ + [.] `Inhabited : some Sort.{?_uniq} @ ⟨39, 11⟩-⟨39, 20⟩ Inhabited : Type → Type @ ⟨39, 11⟩-⟨39, 20⟩ Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1178} @ ⟨39, 21⟩-⟨39, 24⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨39, 21⟩-⟨39, 24⟩ Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩ instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩†-⟨39, 30⟩† instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩-⟨39, 8⟩ @@ -405,14 +401,13 @@ infoTree.lean:44:0: error: expected stx [Elab.info] command @ ⟨41, 0⟩-⟨41, 5⟩ @ no_elab [Elab.info] command @ ⟨44, 0⟩-⟨44, 22⟩ @ Lean.Elab.Command.elabSetOption [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩ -infoTree.lean:46:16: warning: unused variable `y` [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1181} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ _uniq.1182 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1183} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ _uniq.1184 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ Eq.{1} Nat _uniq.1182 _uniq.1182 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» @@ -433,11 +428,11 @@ infoTree.lean:46:16: warning: unused variable `y` _uniq.1190 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1189 _uniq.1190]) f6.f7 : Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1191} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ _uniq.1192 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1193} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ _uniq.1194 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ Eq.{1} Nat _uniq.1192 _uniq.1192 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» @@ -457,10 +452,10 @@ infoTree.lean:46:16: warning: unused variable `y` _uniq.1200 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ _uniq.1201 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ Eq.refl.{1} Nat _uniq.1200 : Eq.{1} Nat _uniq.1200 _uniq.1200 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq.1196} Nat _uniq.1200 _uniq.1200 @ ⟨46, 36⟩-⟨46, 43⟩ + [.] `Eq.refl : some Eq.{?_uniq} Nat _uniq.1200 _uniq.1200 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ _uniq.1200 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent - [.] `x : some ?_uniq.1203 @ ⟨46, 44⟩-⟨46, 45⟩ + [.] `x : some ?_uniq @ ⟨46, 44⟩-⟨46, 45⟩ _uniq.1200 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ [mdata _recApp: _uniq.1199 _uniq.1189 _uniq.1190] : Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp [.] `f7 : some Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨47, 2⟩-⟨47, 4⟩ @@ -475,11 +470,11 @@ infoTree.lean:46:16: warning: unused variable `y` 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.1223} @ ⟨50, 12⟩-⟨50, 13⟩ + [.] `B : some Sort.{?_uniq} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ _uniq.1224 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1225} @ ⟨50, 17⟩-⟨50, 18⟩ + [.] `B : some Sort.{?_uniq} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ _uniq.1226 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ _uniq.1227 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩