From d92948bc20b12f53542814c79469711ceff19fbf Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 1 Aug 2022 05:59:45 -0400 Subject: [PATCH] chore: prune ancient keywords --- doc/expressions.md | 12 ++++++------ doc/highlight.js | 6 +++--- doc/implicit.md | 2 +- doc/latex/lean4.py | 9 ++++----- doc/latex/lstlean.tex | 23 ++++++++++++----------- 5 files changed, 26 insertions(+), 26 deletions(-) diff --git a/doc/expressions.md b/doc/expressions.md index 04e8969315..51242b5d8d 100644 --- a/doc/expressions.md +++ b/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 diff --git a/doc/highlight.js b/doc/highlight.js index ad36345deb..175c05d1e7 100644 --- a/doc/highlight.js +++ b/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 ' + diff --git a/doc/implicit.md b/doc/implicit.md index dcda6a3399..0292464d19 100644 --- a/doc/implicit.md +++ b/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 diff --git a/doc/latex/lean4.py b/doc/latex/lean4.py index c5d10f6cca..a75b26b5a9 100644 --- a/doc/latex/lean4.py +++ b/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', diff --git a/doc/latex/lstlean.tex b/doc/latex/lstlean.tex index c91a9d7e1e..a54d4ba2cf 100644 --- a/doc/latex/lstlean.tex +++ b/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},