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

feat: in trailing command

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-02 09:52:54 -07:00
parent 988bb09aaf
commit bda85f287c
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/Command.lean
View file

@ -97,6 +97,8 @@ def openSimple := parser! many1 ident
@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end"
@[builtinCommandParser] def «in» := tparser! " in " >> commandParser
end Command
end Parser
end Lean