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

chore(frontends/lean/token_table): remove dead keywords

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-07 14:00:49 -08:00
parent c427350dc0
commit 51958df84b
5 changed files with 8 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -11,7 +11,7 @@ import init.meta.lean.parser init.meta.quote
open lean
open lean.parser
local postfix ?:9001 := optional
local postfix `?`:9001 := optional
local postfix *:9001 := many
namespace interactive

2
library/init/meta/lean/parser.lean
View file

@ -56,7 +56,7 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
ys ← many x,
return $ y::ys) <|> pure list.nil
local postfix ?:100 := optional
local postfix `?`:100 := optional
local postfix * := many
meta def sep_by {α : Type} : string → parser α → parser (list α)

2
library/init/meta/smt/interactive.lean
View file

@ -39,7 +39,7 @@ namespace interactive
open lean.parser
open interactive
open interactive.types
local postfix ?:9001 := optional
local postfix `?`:9001 := optional
local postfix *:9001 := many
meta def itactic : Type :=

2
src/frontends/lean/notation_cmd.cpp
View file

@ -90,7 +90,7 @@ using notation::mk_skip_action;
using notation::transition;
using notation::action;
static char const * g_forbidden_tokens[] = {"!", "@", nullptr};
static char const * g_forbidden_tokens[] = {"@", nullptr};
void check_not_forbidden(char const * tk) {
auto it = g_forbidden_tokens;

9
src/frontends/lean/token_table.cpp
View file

@ -88,14 +88,13 @@ void init_token_table(token_table & t) {
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
{"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
{"(:", g_max_prec}, {":)", 0},
{"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
{"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
{"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
{"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
{".", 0}, {":", 0}, {"!", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
{"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
{"@@", g_max_prec}, {"@", g_max_prec},
{"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
{"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
{"~>", g_max_prec+1},
{"match", 0}, {"~>", g_max_prec+1},
{".1", g_max_prec+1}, {".2", g_max_prec+1}, {".3", g_max_prec+1}, {".4", g_max_prec+1}, {".5", g_max_prec+1}, {".6", g_max_prec+1},
{".7", g_max_prec+1}, {".8", g_max_prec+1}, {".9", g_max_prec+1},
{"renaming", 0}, {"extends", 0}, {nullptr, 0}};