michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(*): remove remaining references to by+ and begin+

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-29 13:59:06 -08:00
parent b7b4b6d838
commit f55e456c84
4 changed files with 5 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/emacs/lean-syntax.el
View file

@ -9,7 +9,7 @@
(defconst lean-keywords1
'("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
"hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
"hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
"hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
"print" "theorem" "proposition" "example" "abbreviation" "abstract"
"open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
@ -26,11 +26,6 @@
"lean keywords ending with 'word' (not symbol)")
(defconst lean-keywords1-regexp
(eval `(rx word-start (or ,@lean-keywords1) word-end)))
(defconst lean-keywords2
'("by+" "begin+")
"lean keywords ending with 'symbol'")
(defconst lean-keywords2-regexp
(eval `(rx word-start (or ,@lean-keywords2) symbol-end)))
(defconst lean-constants
'("#" "@" "!" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
"≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ"
@ -170,7 +165,6 @@
(,(rx (or "∘if")) . 'font-lock-constant-face)
;; Keywords
("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
(,lean-keywords2-regexp . 'font-lock-keyword-face)
(,lean-keywords1-regexp . 'font-lock-keyword-face)
(,(rx word-start (group "example") ".") (1 'font-lock-keyword-face))
(,(rx (or "∎")) . 'font-lock-keyword-face)

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

@ -568,7 +568,7 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
// When from_term is not just a constant or local constant, we compile obtain as:
//
// have H : _, from from_term,
// (by+ exact (obtain ps, from H, goal_term)) H
// (by exact (obtain ps, from H, goal_term)) H
//
// Motivation, we want "from_term" (and its type) to be elaborated before processing the
// obtain-expression

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

@ -90,7 +90,7 @@ static char const * g_decreasing_unicode = "↓";
void init_token_table(token_table & t) {
pair<char const *, unsigned> builtin[] =
{{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
{"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
{"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
{"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
@ -99,7 +99,7 @@ void init_token_table(token_table & t) {
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
{"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
{"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
{"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},
{"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
{"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},

2
src/vim/syntax/lean.vim
View file

@ -24,7 +24,7 @@ syn case match
" keywords
syn keyword leanKeyword import prelude tactic_hint protected private noncomputable
syn keyword leanKeyword definition renaming hiding exposing parameter parameters
syn keyword leanKeyword begin "begin+" proof qed conjecture constant constants hypothesis lemma
syn keyword leanKeyword begin proof qed conjecture constant constants hypothesis lemma
syn keyword leanKeyword corollary variable variables premise premises theory print theorem proposition
syn keyword leanKeyword example abbreviation abstract open as export override axiom axioms inductive
syn keyword leanKeyword with structure record universe universes alias help environment options