Use new names for node kinds

See: <leanprover/lean4#1090>

Addresses errors:

```sh-session
$ lean Bigop.lean
bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat
bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat
bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat
bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat
bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat
bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat
bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10
bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10
bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10
bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10
bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10
bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10
bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat
Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal
Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented
Bigop.lean:122:14: error: expected ')'
$ lean Expander.lean
Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier
Expander.lean:134:10: error: expected identifier
Expander.lean:136:10: error: expected identifier
Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal
Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal
Expander.lean:140:20: error: expected '`(tactic|'
Expander.lean:143:20: error: expected '`(tactic|'
Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier
Expander.lean:201:10: error: expected identifier
Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal
Expander.lean:203:20: error: expected '`(tactic|'
Expander.lean:301:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors
Expander.lean:308:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors
```

Bigop.lean

@@ -116,7 +116,7 @@ syntax "def_bigop" str term:max term:max : command
 -- `F` is inserted only in the second expansion, the expansion of the new macro `$head`.
 macro_rules
   | `(def_bigop $head $op $unit) =>
-    `(macro $head:strLit "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F))
+    `(macro $head:str "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F))
 
 def_bigop "SUM" Nat.add 0
 #check SUM (i <- [0, 1, 2]) i+1

Expander.lean

@@ -124,8 +124,8 @@ partial def expand : Syntax → ExpanderM Syntax
   | `(fun $id:ident => $e) => do
     let e ← withLocal (getIdentVal id) (expand e)
     `(fun $id:ident => $e)
-  | `($num:numLit) => `($num:numLit)
-  | `($str:strLit) => `($str:strLit)
+  | `($num:num) => `($num:num)
+  | `($str:str) => `($str:str)
   | `($n:quotedName) => `($n:quotedName)
   | `($fn $args*) => do
     let fn ← expand fn
@@ -195,8 +195,8 @@ partial def pp : Syntax → Format
     | ps => ppIdent id.getId ++ bracket "{" (joinSep (ps.map (format ∘ Prod.fst)) ", ") "}"
   | `(fun ($id : $ty) => $e) => paren f!"fun {paren (pp id ++ " : " ++ pp ty)} => {pp e}"
   | `(fun $id => $e) => paren f!"fun {pp id} => {pp e}"
-  | `($num:numLit) => format (num.isNatLit?.getD 0)
-  | `($str:strLit) => repr (str.isStrLit?.getD "")
+  | `($num:num) => format (num.isNatLit?.getD 0)
+  | `($str:str) => repr (str.isStrLit?.getD "")
   | `($fn $args*) => paren <| pp fn ++ " " ++ joinSep (args.toList.map pp) line
   | `(def $id:ident := $e) => f!"def {ppIdent id.getId} := {pp e}"
   | `(syntax $[(name := $n)]? $[(priority := $prio)]? $[$args:stx]* : $kind) => "syntax ..."  -- irrelevant for this example

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-05
+leanprover/lean4:nightly-2022-04-02