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

chore: remove #preterm

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-05 11:38:53 -08:00
parent 59eb963153
commit 68e18937b2
2 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Lean/Elaborator/Command.lean
View file

@ -190,14 +190,6 @@ fun n => do
runIO (IO.println (toString pos ++ " " ++ toString resolvedIds));
pure ()
@[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
fun n => do
let s := n.getArg 1;
runIO (IO.println s);
pre ← toPreTerm (s.lift Expr);
runIO (IO.println pre.dbgToString);
pure ()
@[builtinCommandElab «elab»] def elabElab : CommandElab :=
fun n => do
let s := n.getArg 1;

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

@ -82,7 +82,6 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def check := parser! "#check " >> termParser
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
@[builtinCommandParser] def «preterm» := parser! "#preterm " >> termParser
@[builtinCommandParser] def «elab» := parser! "#elab " >> termParser
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)