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

feat: add #eval syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-16 10:56:47 +02:00
parent 09eb27404f
commit 1ccaadfcf0
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Parser/Command.lean
View file

@ -80,6 +80,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def «universes» := parser! "universes " >> many1 ident
@[builtinCommandParser] def check := parser! "#check " >> termParser
@[builtinCommandParser] def check_failure := parser! "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtinCommandParser] def eval := parser! "#eval " >> termParser
@[builtinCommandParser] def synth := parser! "#synth " >> termParser
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident