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

feat: add helper macro forIn!

Browse source 
We are going to write a custom elaborator for `forIn` applications.
This commit is contained in:
Leonardo de Moura 2021-02-05 16:36:30 -08:00
parent eb510c16c3
commit e3c3fc3165
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -188,6 +188,8 @@ def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
@[builtinTermParser] def binrel := parser! "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := parser! "forIn! " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := parser! "ensureExpectedType! " >> strLit >> termParser maxPrec