From 73b7a754ee41bc8e9cc4a57cbd19f4303d58007f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 May 2021 15:11:00 -0700 Subject: [PATCH] fix: `let_fun` with patterns --- src/Lean/Elab/Binders.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 9471d20d01..08544376a4 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -607,11 +607,11 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B let type := expandOptType stx optType let val := letDecl[4] let stxNew ← `(let x : $type := $val; match x with | $pat => $body) - let stxNew := match useLetExpr, elabBodyFirst with + let stxNew := match useLetExpr, elabBodyFirst with | true, false => stxNew | true, true => stxNew.setKind `Lean.Parser.Term.«let_delayed» - | false, true => stxNew.setKind `Lean.Parser.Term.«let_fun» - | false, false => unreachable! + | false, false => stxNew.setKind `Lean.Parser.Term.«let_fun» + | false, true => unreachable! withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? else if letDecl.getKind == `Lean.Parser.Term.letEqnsDecl then let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl