From 35d9590b7b866c1330028ccdecfb5c95a458c7fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Sep 2021 22:20:32 -0700 Subject: [PATCH] chore: rename `let_tmp` elaborator --- src/Lean/Elab/Binders.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 84bce7ede7..dfada60b7e 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -632,7 +632,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B @[builtinTermElab «let_delayed»] def elabLetDelayedDecl : TermElab := fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := true) (usedLetOnly := false) -@[builtinTermElab «let_zeta»] def elabLetZetaDecl : TermElab := +@[builtinTermElab «let_tmp»] def elabLetTmpDecl : TermElab := fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := true) builtin_initialize registerTraceClass `Elab.let