From 0c4d72c1d59c2771e79bf6ded67f491f32e98e09 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Mar 2021 15:21:32 -0800
Subject: [PATCH] refactor: add `implicitLambda` argument

---
 src/Lean/Elab/App.lean  |  4 ++--
 src/Lean/Elab/Term.lean | 17 +++++++----------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3e0026283b..6d6caeb989 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -918,8 +918,8 @@ private def elabAtom : TermElab := fun stx expectedType? =>
   match stx with
   | `(@$id:ident)         => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
   | `(@$id:ident.{$us,*}) => elabAtom stx expectedType?
-  | `(@($t))              => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
+  | `(@($t))              => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
   | _                     => throwUnsupportedSyntax
 
 @[builtinTermElab choice] def elabChoice : TermElab := elabAtom
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 2ff4d3b68d..eccb5b2bd2 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1042,15 +1042,12 @@ def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
   and returned.
   The option `catchExPostpone == false` is used to implement `resumeElabTerm`
   to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
-def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
-  withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone true stx) (mkTermInfo stx)
+def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
+  withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx) (mkTermInfo stx)
 
-def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
-  let e ← elabTerm stx expectedType? catchExPostpone
-  withRef stx $ ensureHasType expectedType? e errorMsgHeader?
-
-def elabTermWithoutImplicitLambdas (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := do
-  elabTermAux expectedType? catchExPostpone false stx
+def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
+  let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
+  withRef stx <| ensureHasType expectedType? e errorMsgHeader?
 
 /-- Adapt a syntax transformation to a regular, term-producing elaborator. -/
 def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expectedType? => do
@@ -1407,12 +1404,12 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | some msg => do
     let refTerm ← elabTerm stx[1] none
     let refTermType ← inferType refTerm
-    elabTermEnsuringType stx[3] refTermType true msg
+    elabTermEnsuringType stx[3] refTermType (errorMsgHeader? := msg)
 
 @[builtinTermElab ensureExpectedType] def elabEnsureExpectedType : TermElab := fun stx expectedType? =>
   match stx[1].isStrLit? with
   | none     => throwIllFormedSyntax
-  | some msg => elabTermEnsuringType stx[2] expectedType? true msg
+  | some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
 
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
   let openDecls ← elabOpenDecl stx[1]