From 9d34d9bc5a41bdbd7444bd325297656c8442e180 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Feb 2022 17:01:21 -0800 Subject: [PATCH] feat: cache and optimize `mkCongrSimp?` at `simp` see #988 --- src/Lean/Meta/CongrTheorems.lean | 75 ++++++++-------- src/Lean/Meta/Tactic/Simp/Main.lean | 17 +++- src/Lean/Meta/Tactic/Simp/Types.lean | 8 +- tests/lean/infoTree.lean.expected.out | 118 +++++++++++++------------- 4 files changed, 116 insertions(+), 102 deletions(-) diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 93c7b924bc..9bf1cb671b 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -160,12 +160,44 @@ private def hasCastLike (kinds : Array CongrArgKind) : Bool := private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do forallBoundedTelescope type (some 1) fun xs type => k xs[0] type +/-- + Test whether we should use `subsingletonInst` kind for instances which depend on `eq`. + (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/ +private def shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do + if info.paramInfo[i].isDecInst then + for j in info.paramInfo[i].backDeps do + if kinds[j] matches CongrArgKind.eq then + return true + return false + +def getCongrSimpKinds (info : FunInfo) : Array CongrArgKind := Id.run do + /- The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this + argument. However, if there are references from `i` to `j`, we cannot + rewrite both `i` and `j`. So we must change the `CongrArgKind` at + either `i` or `j`. In principle, if there is a dependency with `i` + appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is + an optimization: if `i` is a subsingleton, we can fix it instead of + `j`, since all subsingletons are equal anyway. The fixing happens in + two loops: one for the special cases, and one for the general case. -/ + let mut result := #[] + for i in [:info.paramInfo.size] do + if info.resultDeps.contains i then + result := result.push CongrArgKind.fixed + else if info.paramInfo[i].isProp then + result := result.push CongrArgKind.cast + else if info.paramInfo[i].isInstImplicit then + if shouldUseSubsingletonInst info result i then + result := result.push CongrArgKind.subsingletonInst + else + result := result.push CongrArgKind.fixed + else + result := result.push CongrArgKind.eq + return fixKindsForDependencies info result + /-- Create a congruence theorem that is useful for the simplifier. -/ -partial def mkCongrSimpWithArity? (f : Expr) (numArgs : Nat) : MetaM (Option CongrTheorem) := do - let info ← getFunInfo f - let kinds := getKinds info +partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do if let some result ← mk? f info kinds then return some result else if hasCastLike kinds then @@ -246,41 +278,8 @@ where mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq) go 0 type - getKinds (info : FunInfo) : Array CongrArgKind := Id.run do - /- The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this - argument. However, if there are references from `i` to `j`, we cannot - rewrite both `i` and `j`. So we must change the `CongrArgKind` at - either `i` or `j`. In principle, if there is a dependency with `i` - appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is - an optimization: if `i` is a subsingleton, we can fix it instead of - `j`, since all subsingletons are equal anyway. The fixing happens in - two loops: one for the special cases, and one for the general case. -/ - let mut result := #[] - for i in [:info.paramInfo.size] do - if info.resultDeps.contains i then - result := result.push CongrArgKind.fixed - else if info.paramInfo[i].isProp then - result := result.push CongrArgKind.cast - else if info.paramInfo[i].isInstImplicit then - if shouldUseSubsingletonInst info result i then - result := result.push CongrArgKind.subsingletonInst - else - result := result.push CongrArgKind.fixed - else - result := result.push CongrArgKind.eq - return fixKindsForDependencies info result - - /-- - Test whether we should use `subsingletonInst` kind for instances which depend on `eq`. - (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/ - shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do - if info.paramInfo[i].isDecInst then - for j in info.paramInfo[i].backDeps do - if kinds[j] matches CongrArgKind.eq then - return true - return false - def mkCongrSimp? (f : Expr) : MetaM (Option CongrTheorem) := do - mkCongrSimpWithArity? f (← getFunInfo f).getArity + let info ← getFunInfo f + mkCongrSimpCore? f info (getCongrSimpKinds info) end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index ba75d27543..4825b57338 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -262,15 +262,26 @@ where proof ← Meta.mkCongrFun proof arg return { expr := eNew, proof? := proof } + mkCongrSimp? (f : Expr) : M (Option CongrTheorem) := do + let info ← getFunInfo f + let kinds := getCongrSimpKinds info + if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then + /- If all argument kinds are `fixed` or `eq`, then using + simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof -/ + return none + match (← get).congrCache.find? f with + | some thm? => return thm? + | none => + let thm? ← mkCongrSimpCore? f info kinds + modify fun s => { s with congrCache := s.congrCache.insert f thm? } + return thm? + /-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`. -/ tryAutoCongrTheorem? (e : Expr) : M (Option Result) := do if (← isMatcherApp e) then return none let f := e.getAppFn -- TODO: cache let some cgrThm ← mkCongrSimp? f | return none - if cgrThm.argKinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then - -- If all argument kinds are `fixed` or `eq`, then using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof - return none if cgrThm.argKinds.size != e.getAppNumArgs then return none let mut simplified := false let mut hasProof := false diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 975119dc1b..fdb314f5f3 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Meta.AppBuilder +import Lean.Meta.CongrTheorems import Lean.Meta.Tactic.Simp.SimpTheorems import Lean.Meta.Tactic.Simp.SimpCongrTheorems @@ -17,6 +18,8 @@ structure Result where abbrev Cache := ExprMap Result +abbrev CongrCache := ExprMap (Option CongrTheorem) + structure Context where config : Config := {} simpTheorems : SimpTheorems := {} @@ -29,8 +32,9 @@ def Context.mkDefault : MetaM Context := return { config := {}, simpTheorems := (← getSimpTheorems), congrTheorems := (← getSimpCongrTheorems) } structure State where - cache : Cache := {} - numSteps : Nat := 0 + cache : Cache := {} + congrCache : CongrCache := {} + numSteps : Nat := 0 abbrev SimpM := ReaderT Context $ StateRefT State MetaM diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index eb958ced86..7e20c0a9c6 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -112,20 +112,20 @@ [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.619} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.567} @ ⟨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.621} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.569} @ ⟨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.624} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.572} @ ⟨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.626} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.574} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ fun x y b => let x := (x + y, x - y); @@ -238,10 +238,10 @@ Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.824} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.772} @ ⟨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.823} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.771} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -249,17 +249,17 @@ ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.825} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.773} @ ⟨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.826} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.774} @ ⟨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.828} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.776} @ ⟨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.829} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.777} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ 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, 17⟩ @ Lean.Elab.Term.elabApp @@ -275,11 +275,11 @@ 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.870} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.818} @ ⟨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.872} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.820} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp @@ -294,11 +294,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.892} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.840} @ ⟨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.894} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.842} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst @@ -338,73 +338,73 @@ 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.915} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.863} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.916 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.864 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.917} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.865} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.918 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.916 _uniq.916 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.866 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + Eq.{1} Nat _uniq.864 _uniq.864 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x) - Eq.{1} Nat _uniq.916 _uniq.916 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel - _uniq.916 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent - _uniq.916 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.916 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent - _uniq.916 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.925 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ - _uniq.926 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.925 _uniq.926]) f6.f7 : Eq.{1} Nat _uniq.925 _uniq.925 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec + Eq.{1} Nat _uniq.864 _uniq.864 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel + _uniq.864 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + _uniq.864 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ + _uniq.864 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + _uniq.864 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ + _uniq.873 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.874 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.873 _uniq.874]) f6.f7 : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.927} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.875} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.928 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.876 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.929} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.877} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.930 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.928 _uniq.928 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.878 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.{1} Nat _uniq.876 _uniq.876 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x) - Eq.{1} Nat _uniq.928 _uniq.928 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel - _uniq.928 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent - _uniq.928 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.928 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent - _uniq.928 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.935 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ - _uniq.938 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ - _uniq.939 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.refl.{1} Nat _uniq.938 : Eq.{1} Nat _uniq.938 _uniq.938 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq.932} Nat _uniq.938 _uniq.938 @ ⟨46, 36⟩-⟨46, 43⟩ + Eq.{1} Nat _uniq.876 _uniq.876 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel + _uniq.876 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent + _uniq.876 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ + _uniq.876 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent + _uniq.876 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ + _uniq.883 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ + _uniq.886 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.887 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.refl.{1} Nat _uniq.886 : Eq.{1} Nat _uniq.886 _uniq.886 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp + [.] `Eq.refl : some Eq.{?_uniq.880} Nat _uniq.886 _uniq.886 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ - _uniq.938 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent - _uniq.938 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ - [mdata _recApp: _uniq.935 _uniq.925 _uniq.926] : Eq.{1} Nat _uniq.925 _uniq.925 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp - _uniq.935 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.925 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent - _uniq.925 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.926 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent - _uniq.926 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ + _uniq.886 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent + _uniq.886 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ + [mdata _recApp: _uniq.883 _uniq.873 _uniq.874] : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp + _uniq.883 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.873 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent + _uniq.873 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ + _uniq.874 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent + _uniq.874 : 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.962} @ ⟨50, 12⟩-⟨50, 13⟩ + [.] `B : some Sort.{?_uniq.910} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ - _uniq.963 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + _uniq.911 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.964} @ ⟨50, 17⟩-⟨50, 18⟩ + [.] `B : some Sort.{?_uniq.912} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ - _uniq.967 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ - B.mk (B.pair _uniq.967) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst - B.pair _uniq.967 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj - _uniq.967 : B @ ⟨50, 24⟩-⟨50, 25⟩ - [.] _uniq.967 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A + _uniq.915 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + B.mk (B.pair _uniq.915) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst + B.pair _uniq.915 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj + _uniq.915 : B @ ⟨50, 24⟩-⟨50, 25⟩ + [.] _uniq.915 : 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.967 @ ⟨50, 22⟩†-⟨50, 32⟩ + pair : Prod.{0 0} A A := B.pair _uniq.915 @ ⟨50, 22⟩†-⟨50, 32⟩ f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩