From 1ccaadfcf069d9d4ef52314b1f2fb8d49a09c5ec Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Jun 2020 10:56:47 +0200 Subject: [PATCH] feat: add `#eval` syntax --- src/Lean/Parser/Command.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 1f0d5dc33d..685767706f 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -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