max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: let_zeta => let_tmp

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-30 22:19:06 -07:00
parent 035251d08a
commit 2bc24ff619
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Term.lean
View file

@ -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