From 26a565496e6eb41ed2f14bf43bacdc02587e2d5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jul 2022 14:19:06 -0700
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Elab/App.lean | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 81d0e437f9..420c79708a 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -877,13 +877,6 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
   trace[Elab.app.args] "explicit: {explicit}, ellipsis: {ellipsis}, {f} : {fType}"
   trace[Elab.app.args] "namedArgs: {namedArgs}"
   trace[Elab.app.args] "args: {args}"
-  let go (namedArgs : Array NamedArg) (args : Array Arg) : TermElabM Expr := do
-    ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' {
-      args := args.toList
-      expectedType?, f, fType
-      namedArgs := namedArgs.toList
-      propagateExpected := (← propagateExpectedTypeFor f)
-    }
   if let some elimInfo ← elabAsElim? then
     tryPostponeIfNoneOrMVar expectedType?
     let some expectedType := expectedType? | throwError "failed to elaborate eliminator, expected type is not available"