diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 7f8bc0b407..ba62e40ef2 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -47,9 +47,6 @@ def back [Inhabited α] (a : Array α) : α := def get? (a : Array α) (i : Nat) : Option α := if h : i < a.size then some a[i] else none -abbrev getOp? (self : Array α) (idx : Nat) : Option α := - self.get? idx - def back? (a : Array α) : Option α := a.get? (a.size - 1) diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 32de1a97f1..343706cd49 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -29,9 +29,6 @@ def get (s : Subarray α) (i : Fin s.size) : α := exact Nat.add_lt_of_lt_sub this s.as[s.start + i.val] -abbrev getOp (self : Subarray α) (idx : Fin self.size) : α := - self.get idx - instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where getElem xs i h := xs.get ⟨i, h⟩ @@ -41,9 +38,6 @@ instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α := getD s i default -abbrev getOp! [Inhabited α] (self : Subarray α) (idx : Nat) : α := - self.get! idx - def popFront (s : Subarray α) : Subarray α := if h : s.start < s.stop then { s with start := s.start + 1, h₁ := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) } diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 534007331a..c7b8b1be15 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -49,9 +49,6 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8 def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8 | ⟨bs⟩, i => bs.get i -@[inline] def getOp (self : ByteArray) (idx : Nat) : UInt8 := - self.get! idx - instance : GetElem ByteArray Nat UInt8 fun xs i => LT.lt i xs.size where getElem xs i h := xs.get ⟨i, h⟩ diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index 4864f74952..2769b94b28 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -55,9 +55,6 @@ def get? (ds : FloatArray) (i : Nat) : Option Float := else none -@[inline] def getOp (self : FloatArray) (idx : Nat) : Float := - self.get! idx - instance : GetElem FloatArray Nat Float fun xs i => LT.lt i xs.size where getElem xs i h := xs.get ⟨i, h⟩ diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 4bf6e539c1..a9f850bce5 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -66,9 +66,6 @@ private def utf8GetAux? : List Char → Pos → Pos → Option Char def get? : (@& String) → (@& Pos) → Option Char | ⟨s⟩, p => utf8GetAux? s 0 p -abbrev getOp? (self : String) (idx : Pos) : Option Char := - self.get? idx - /-- Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`. -/ @@ -77,9 +74,6 @@ def get! (s : @& String) (p : @& Pos) : Char := match s with | ⟨s⟩ => utf8GetAux s 0 p -abbrev getOp! (self : String) (idx : Pos) : Char := - self.get! idx - private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char | [], _, _ => [] | c::cs, i, p => diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index a7b0db3c20..57b796b8a0 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1269,12 +1269,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α := def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α := Array.getD a i default -abbrev Array.getOp {α : Type u} (self : Array α) (idx : Fin self.size) : α := - self.get idx - -abbrev Array.getOp! {α : Type u} [Inhabited α] (self : Array α) (idx : Nat) : α := - self.get! idx - instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where getElem xs i h := xs.get ⟨i, h⟩ @@ -1917,10 +1911,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax := | Syntax.node _ _ args => args.getD i Syntax.missing | _ => Syntax.missing --- Add `stx[i]` as sugar for `stx.getArg i` -@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax := - self.getArg idx - instance : GetElem Syntax Nat Syntax fun _ _ => True where getElem stx i _ := stx.getArg i diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 57d5bc3796..1a53ae9b23 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -375,9 +375,9 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl /-- Auxiliary datatatype for presenting a Lean lvalue modifier. We represent a unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`. - Example: `a.foo[i].1` is represented as the `Syntax` `a` and the list - `[LVal.fieldName "foo", LVal.getOp i, LVal.fieldIdx 1]`. - Recall that the notation `a[i]` is not just for accessing arrays in Lean. -/ + Example: `a.foo.1` is represented as the `Syntax` `a` and the list + `[LVal.fieldName "foo", LVal.fieldIdx 1]`. +-/ inductive LVal where | fieldIdx (ref : Syntax) (i : Nat) /- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name. diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index bae921ab0d..f0fa09d841 100644 --- a/src/Std/Data/HashMap.lean +++ b/src/Std/Data/HashMap.lean @@ -178,9 +178,6 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool := | some b => b | none => panic! "key is not in the map" -@[inline] def getOp (self : HashMap α β) (idx : α) : Option β := - self.find? idx - instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where getElem m k _ := m.find? k diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index a42a3831ce..a3d578c86d 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -63,9 +63,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α := else getAux t.root (USize.ofNat i) t.shift -def getOp [Inhabited α] (self : PersistentArray α) (idx : Nat) : α := - self.get! idx - -- TODO: remove [Inhabited α] instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where getElem xs i _ := xs.get! i diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean index 95d6ed422c..9392c42fb7 100644 --- a/src/Std/Data/PersistentHashMap.lean +++ b/src/Std/Data/PersistentHashMap.lean @@ -146,9 +146,6 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β | { root := n, .. }, k => findAux n (hash k |>.toUSize) k -@[inline] def getOp {_ : BEq α} {_ : Hashable α} (self : PersistentHashMap α β) (idx : α) : Option β := - self.find? idx - instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where getElem m i _ := m.find? i diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index b67bef90fb..e460333a89 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -297,26 +297,38 @@ 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⟩ - Array.push (Array.getOp! s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabApp - [.] `s : some Array.{0} Nat @ ⟨28, 2⟩-⟨28, 3⟩ - s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ - @Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩ - @Array.getOp! : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩ - 1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩ @ Lean.Elab.Term.elabNumLit - [.] Array.getOp! s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ : some Array.{0} Nat + Array.push (getElem! s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 18⟩ @ Lean.Elab.Term.elabApp + getElem! s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 9⟩ @ «_aux_Init_Util___macroRules_term__[_]_!_1» + Macro expansion + s.2[1]! + ===> + getElem!✝ s.2 1 + getElem! s.snd 1 : Array Nat @ ⟨28, 2⟩†-⟨28, 7⟩ @ Lean.Elab.Term.elabApp + [.] `getElem!._@.infoTree._hyg.139 : none @ ⟨28, 2⟩†-⟨28, 9⟩† + @getElem! : {Cont Idx Elem : Type} → + {Dom : Cont → Idx → Prop} → + [inst : GetElem Cont Idx Elem Dom] → + [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.777 @ ⟨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 + [.] getElem! 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.805 @ ⟨28, 15⟩-⟨28, 16⟩ + [.] `s : some ?_uniq.1069 @ ⟨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.812} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.1081} @ ⟨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.814} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.1083} @ ⟨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⟩ @@ -333,11 +345,11 @@ f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ [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.834} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.1103} @ ⟨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.836} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.1105} @ ⟨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⟩ @@ -348,7 +360,7 @@ ===> Prod.mk✝ { val := id } { val := id } ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp - [.] `Prod.mk._@.infoTree._hyg.152 : some Prod.{0 0} A A @ ⟨34, 10⟩†-⟨34, 40⟩† + [.] `Prod.mk._@.infoTree._hyg.156 : some Prod.{0 0} A A @ ⟨34, 10⟩†-⟨34, 40⟩† @Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩† { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩ @ Lean.Elab.Term.elabIdent @@ -383,87 +395,87 @@ infoTree.lean:44:0: error: expected stx [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩ [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.857} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.1126} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.858 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.1127 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.859} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.1128} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.860 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.1129 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + Eq.{1} Nat _uniq.1127 _uniq.1127 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> - (Term.binrel "binrel%" `Eq._@.infoTree._hyg.176 `x `x) - Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel - [.] `Eq._@.infoTree._hyg.176 : none @ ⟨45, 21⟩†-⟨45, 26⟩† - _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + (Term.binrel "binrel%" `Eq._@.infoTree._hyg.180 `x `x) + Eq.{1} Nat _uniq.1127 _uniq.1127 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel + [.] `Eq._@.infoTree._hyg.180 : none @ ⟨45, 21⟩†-⟨45, 26⟩† + _uniq.1127 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + _uniq.1127 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ + _uniq.1127 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.864 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ - _uniq.865 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ - _uniq.866 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.865 _uniq.866]) f6.f7 : Eq.{1} Nat _uniq.865 _uniq.865 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec + _uniq.1127 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ + _uniq.1133 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ + _uniq.1134 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.1135 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1134 _uniq.1135]) f6.f7 : Eq.{1} Nat _uniq.1134 _uniq.1134 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.867} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.1136} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.868 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.1137 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.869} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.1138} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.870 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.868 _uniq.868 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.1139 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.{1} Nat _uniq.1137 _uniq.1137 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> - (Term.binrel "binrel%" `Eq._@.infoTree._hyg.184 `x `x) - Eq.{1} Nat _uniq.868 _uniq.868 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel - [.] `Eq._@.infoTree._hyg.184 : none @ ⟨46, 27⟩†-⟨46, 32⟩† - _uniq.868 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent + (Term.binrel "binrel%" `Eq._@.infoTree._hyg.188 `x `x) + Eq.{1} Nat _uniq.1137 _uniq.1137 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel + [.] `Eq._@.infoTree._hyg.188 : none @ ⟨46, 27⟩†-⟨46, 32⟩† + _uniq.1137 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.868 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.868 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent + _uniq.1137 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ + _uniq.1137 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.868 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.875 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ - _uniq.876 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ - _uniq.877 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.refl.{1} Nat _uniq.876 : Eq.{1} Nat _uniq.876 _uniq.876 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq.872} Nat _uniq.876 _uniq.876 @ ⟨46, 36⟩-⟨46, 43⟩ + _uniq.1137 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ + _uniq.1144 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ + _uniq.1145 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.1146 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.refl.{1} Nat _uniq.1145 : Eq.{1} Nat _uniq.1145 _uniq.1145 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp + [.] `Eq.refl : some Eq.{?_uniq.1141} Nat _uniq.1145 _uniq.1145 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ - _uniq.876 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent - [.] `x : some ?_uniq.879 @ ⟨46, 44⟩-⟨46, 45⟩ - _uniq.876 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ - [mdata _recApp: _uniq.875 _uniq.865 _uniq.866] : Eq.{1} Nat _uniq.865 _uniq.865 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp - [.] `f7 : some Eq.{1} Nat _uniq.865 _uniq.865 @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.875 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.865 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent + _uniq.1145 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent + [.] `x : some ?_uniq.1148 @ ⟨46, 44⟩-⟨46, 45⟩ + _uniq.1145 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ + [mdata _recApp: _uniq.1144 _uniq.1134 _uniq.1135] : Eq.{1} Nat _uniq.1134 _uniq.1134 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp + [.] `f7 : some Eq.{1} Nat _uniq.1134 _uniq.1134 @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.1144 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.1134 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent [.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.865 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.866 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent + _uniq.1134 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ + _uniq.1135 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent [.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩ - _uniq.866 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ + _uniq.1135 : 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.899} @ ⟨50, 12⟩-⟨50, 13⟩ + [.] `B : some Sort.{?_uniq.1168} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ - _uniq.900 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + _uniq.1169 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.901} @ ⟨50, 17⟩-⟨50, 18⟩ + [.] `B : some Sort.{?_uniq.1170} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ - _uniq.902 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ - _uniq.903 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ - B.mk (B.pair _uniq.903) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst - _uniq.903 : B @ ⟨50, 24⟩-⟨50, 25⟩ - B.pair _uniq.903 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj + _uniq.1171 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ + _uniq.1172 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + B.mk (B.pair _uniq.1172) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst + _uniq.1172 : B @ ⟨50, 24⟩-⟨50, 25⟩ + B.pair _uniq.1172 : 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.903 : B @ ⟨50, 24⟩-⟨50, 25⟩ - [.] _uniq.903 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A + _uniq.1172 : B @ ⟨50, 24⟩-⟨50, 25⟩ + [.] _uniq.1172 : 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.903 @ ⟨50, 22⟩†-⟨50, 32⟩ + pair : Prod.{0 0} A A := B.pair _uniq.1172 @ ⟨50, 22⟩†-⟨50, 32⟩ f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩