From 2bc24ff619e595cac8a164535091e7207c874a02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Sep 2021 22:19:06 -0700 Subject: [PATCH] chore: `let_zeta` => `let_tmp` --- src/Lean/Parser/Term.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 17b07b7961..d72dc07ae9 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -175,8 +175,8 @@ def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll @[builtinTermParser] def «let» := leading_parser:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser @[builtinTermParser] def «let_fun» := leading_parser:leadPrec withPosition ((symbol "let_fun " <|> "let_λ") >> letDecl) >> optSemicolon termParser @[builtinTermParser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser --- `let`-declaration that is expanded after elaboration -@[builtinTermParser] def «let_zeta» := leading_parser:leadPrec withPosition ("let_zeta " >> letDecl) >> optSemicolon termParser +-- `let`-declaration that is only included in the elaborated term if variable is still there +@[builtinTermParser] def «let_tmp» := leading_parser:leadPrec withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser -- like `let_fun` but with optional name def haveIdLhs := optional (ident >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder))) >> optType