chore: prune ancient keywords

doc/expressions.md

@@ -222,7 +222,7 @@ def f2 (a b c : Bool) : Bool :=
 def p : Nat × Bool := (1, false)
 
 section
-variables (a b c : Nat) (p : Nat × bool)
+variable (a b c : Nat) (p : Nat × bool)
 
 #check (1, 2)
 #check p.1 * 2
@@ -232,8 +232,8 @@ end
 
 /- lists -/
 section
-variables x y z : Nat
-variables xs ys zs : list Nat
+variable x y z : Nat
+variable xs ys zs : list Nat
 open list
 
 #check (1 :: xs) ++ (y :: zs) ++ [1,2,3]
@@ -243,7 +243,7 @@ end
 
 /- sets -/
 section
-variables s t u : set Nat
+variable s t u : set Nat
 
 #check ({1, 2, 3} ∩ s) ∪ ({x | x < 7} ∩ t)
 end
@@ -276,7 +276,7 @@ Finally, for data types with one constructor, one destruct an element by pattern
 .. code-block:: lean
 
     universes u v
-    variables {α : Type u} {β : Type v}
+    variable {α : Type u} {β : Type v}
 
     def p : Nat × ℤ := ⟨1, 2⟩
     #check p.fst
@@ -369,7 +369,7 @@ Here is an example:
 
 .. code-block:: lean
 
-    variables (a b c d e : Nat)
+    variable (a b c d e : Nat)
     variable h1 : a = b
     variable h2 : b = c + 1
     variable h3 : c = d

doc/highlight.js

@@ -1111,9 +1111,9 @@ hljs.registerLanguage("lean", function(hljs) {
       'axiom constant ' +
       'partial unsafe private protected ' +
       'if then else ' +
-      'universe variable variables ' +
-      'import open export theory prelude renaming hiding exposing ' +
-      'calc  match with do by let extends ' +
+      'universe variable ' +
+      'import open export prelude renaming hiding ' +
+      'calc match with do by let extends ' +
       'for in unless try catch finally mutual mut return continue break where rec ' +
       'syntax macro_rules macro deriving ' +
       'fun ' +

doc/implicit.md

@@ -64,7 +64,7 @@ It makes these three arguments implicit. Notationally, this hides the specificat
 making it look as though ``compose`` simply takes 3 arguments.
 
 Variables can also be specified as implicit when they are declared with
-the ``variables`` command:
+the ``variable`` command:
 
 ```lean
 universe u

doc/latex/lean4.py

@@ -33,14 +33,13 @@ class Lean4Lexer(RegexLexer):
 
     keywords1 = (
         'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
-        'renaming', 'inline', 'hiding', 'exposing', 'parameter', 'parameters',
-        'conjecture', 'hypothesis', 'lemma', 'corollary', 'variable', 'variables',
+        'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
         'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
-        'help', 'options', 'precedence', 'postfix', 'prefix', 'calc_trans',
-        'calc_subst', 'calc_refl', 'infix', 'infixl', 'infixr', 'notation', '#eval',
+        'help', 'options', 'precedence', 'postfix', 'prefix',
+        'infix', 'infixl', 'infixr', 'notation', '#eval',
         '#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace',
         'including', 'instance', 'section', 'context', 'protected', 'expose',
-        'export', 'set_option', 'add_rewrite', 'extends', 'open', 'example',
+        'export', 'set_option', 'extends', 'open', 'example',
         'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
         'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where',
         'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual',

doc/latex/lstlean.tex

@@ -12,21 +12,22 @@ texcl=false,
 % keywords, list taken from lean-syntax.el
 morekeywords=[1]{
 import, prelude, protected, private, noncomputable, definition, meta, renaming,
-hiding, exposing, parameter, parameters, begin, conjecture, constant, constants,
-hypothesis, lemma, corollary, variable, variables, premise, premises, theory,
-print, theorem, proposition, example,
-open, as, export, override, axiom, axioms, inductive, with, without,
+hiding, parameter, parameters, begin, constant, constants,
+lemma, variable, variables, theory,
+print, theorem, example,
+open, as, export, override, axiom, axioms, inductive, with,
 structure, record, universe, universes,
 alias, help, precedence, reserve, declare_trace, add_key_equivalence,
 match, infix, infixl, infixr, notation, postfix, prefix, instance,
-eval, vm_eval, check, coercion, end, this, suppose,
-using, using_well_founded, namespace, section, fields,
-attribute, local, set_option, extends, include, omit, classes, class,
-instances, coercions, attributes, raw, replacing,
+eval, reduce, check, end, this,
+using, using_well_founded, namespace, section,
+attribute, local, set_option, extends, include, omit, class,
+raw, replacing,
 calc, have, show, suffices, by, in, at, let, forall, Pi, fun,
-exists, if, dif, then, else, assume, obtain, from, aliases, register_simp_ext, unless, break, continue,
-mutual, do, def, run_cmd, const
-partial,mut,where,macro,syntax,deriving, return, try, catch, for, macro_rules,declare_syntax_cat,abbrev},
+exists, if, dif, then, else, assume, obtain, from, register_simp_ext, unless, break, continue,
+mutual, do, def, run_cmd, const,
+partial, mut, where, macro, syntax, deriving,
+return, try, catch, for, macro_rules, declare_syntax_cat, abbrev},
 
 % Sorts
 morekeywords=[2]{Sort, Type, Prop},