From 771e8ad78567966615530f9359f7ab4372a8da7d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Oct 2023 12:19:57 -0700
Subject: [PATCH 1/8] feat: Allow trailing comma in tuples

---
 src/Lean/Parser/Term.lean              | 4 ++--
 tests/compiler/tuple.lean              | 6 ++++++
 tests/compiler/tuple.lean.expected.out | 1 +
 3 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 tests/compiler/tuple.lean
 create mode 100644 tests/compiler/tuple.lean.expected.out

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 7c5c28e4438a..de5162f90809 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -164,7 +164,7 @@ do not yield the right result.
   "(" >> (withoutPosition (withoutForbidden (termParser >> " :" >> optional (ppSpace >> termParser)))) >> ")"
 /-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/
 @[builtin_term_parser] def tuple := leading_parser
-  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", "))) >> ")"
+  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
 Can also be used for creating simple functions when combined with `·`. Here are some examples:
@@ -184,7 +184,7 @@ are turned into a new anonymous constructor application. For example,
 `⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
 -/
 @[builtin_term_parser] def anonymousCtor := leading_parser
-  "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", ")) >> "⟩"
+  "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
 def optIdent : Parser :=
   optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser
diff --git a/tests/compiler/tuple.lean b/tests/compiler/tuple.lean
new file mode 100644
index 000000000000..5fd0be76a63b
--- /dev/null
+++ b/tests/compiler/tuple.lean
@@ -0,0 +1,6 @@
+
+@[noinline] def f (a : Nat × Nat × Nat) : Nat:=
+  a.fst + a.snd.fst + a.snd.snd
+
+def main : IO Unit := do
+  IO.println (f (1, 2, 3,))
diff --git a/tests/compiler/tuple.lean.expected.out b/tests/compiler/tuple.lean.expected.out
new file mode 100644
index 000000000000..1e8b31496214
--- /dev/null
+++ b/tests/compiler/tuple.lean.expected.out
@@ -0,0 +1 @@
+6

From 9e9790d19460252354b90516ec230cf0fa57d911 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Oct 2023 14:17:04 -0700
Subject: [PATCH 2/8] feat: Allow trailing commas in lists

---
 src/Init/Notation.lean                 | 14 ++++++++++----
 tests/compiler/array.lean              |  4 ++++
 tests/compiler/array.lean.expected.out |  1 +
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index fa1d400ff240..367749572632 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -471,7 +471,7 @@ which uses let bindings as intermediates as in
 Note that this changes the order of evaluation, although it should not be observable
 unless you use side effecting operations like `dbg_trace`.
 -/
-syntax "[" withoutPosition(term,*) "]"  : term
+syntax "[" withoutPosition(term,*,?) "]"  : term
 
 /--
 Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
@@ -479,20 +479,26 @@ The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
 It uses binary partitioning to construct a tree of intermediate let bindings as in
 `let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
 -/
-syntax "%[" withoutPosition(term,* " | " term) "]" : term
+syntax "%[" withoutPosition(term,*,? " | " term) "]" : term
 
 namespace Lean
 
 macro_rules
   | `([ $elems,* ]) => do
     -- NOTE: we do not have `TSepArray.getElems` yet at this point
+    let rec isEven (i: Nat) :=
+      match i with
+      | 0 => true
+      | 1 => false
+      | i + 2 => isEven i
     let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
       match i, skip with
       | 0,   _     => pure result
       | i+1, true  => expandListLit i false result
       | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
-    if elems.elemsAndSeps.size < 64 then
-      expandListLit elems.elemsAndSeps.size false (← ``(List.nil))
+    let size := elems.elemsAndSeps.size
+    if size < 64 then
+      expandListLit size (isEven size) (← ``(List.nil))
     else
       `(%[ $elems,* | List.nil ])
 
diff --git a/tests/compiler/array.lean b/tests/compiler/array.lean
index d0bfc5e0a8ca..428c39bd385e 100644
--- a/tests/compiler/array.lean
+++ b/tests/compiler/array.lean
@@ -11,3 +11,7 @@ def main : IO Unit := do
   IO.println (f #[2, 3, 4])
   IO.println (g #[2, 3, 4])
   IO.println (h [2, 3, 4])
+
+  -- Trailing comma
+  --IO.println (g #[5, 6, 7,])
+  IO.println (h [5, 6, 7,])
diff --git a/tests/compiler/array.lean.expected.out b/tests/compiler/array.lean.expected.out
index 04a03c85a0dd..ec095e485b5c 100644
--- a/tests/compiler/array.lean.expected.out
+++ b/tests/compiler/array.lean.expected.out
@@ -1,3 +1,4 @@
 3
 [2, 3, 4]
 [2, 3, 4]
+[5, 6, 7]

From 5f8d488c346530f7973ccd45e4407e04afc50c2a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Oct 2023 14:45:02 -0700
Subject: [PATCH 3/8] fix: Single test failure due to trailing comma

---
 tests/lean/StxQuot.lean.expected.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index eccd27305301..6d637afa3006 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -6,7 +6,7 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
-StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
+"(«term[_]» \"[\" [`x._@.UnhygienicMain._hyg.1 \",\"] \"]\")"
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"

From fab8b65b5111af522dd1ad5550092e7655c54f39 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 18 Oct 2023 15:31:09 -0700
Subject: [PATCH 4/8] feat: Allow trailing commas in simp and rewrite

---
 src/Init/Tactics.lean     | 6 +++---
 tests/lean/rewrite.lean   | 2 +-
 tests/lean/run/simp5.lean | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index cc4272d20373..5e836be03360 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -435,14 +435,14 @@ non-dependent hypotheses. It has many variants:
   other hypotheses.
 -/
 syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 /--
 `simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
 are simplified multiple times until no simplification is applicable.
 Only non-dependent propositional hypotheses are considered.
 -/
 syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : tactic
+  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
 
 /--
 The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only
@@ -450,7 +450,7 @@ applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
 definitionally equal to the input.
 -/
 syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? (location)? : tactic
+  (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
 /--
 `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index 80dc3bb54c88..357055beacc6 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -34,7 +34,7 @@ subst y;
 exact rfl
 
 theorem ex4 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
-rewrite [appendAssoc] at *; -- Error
+rewrite [appendAssoc,] at *; -- Error
 done
 
 theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
index ab7edaa8c440..b7f652026051 100644
--- a/tests/lean/run/simp5.lean
+++ b/tests/lean/run/simp5.lean
@@ -9,6 +9,6 @@ theorem ex1 (a b c : α) : f (f a b) c = a := by
 #print ex1
 
 theorem ex2 (p : Nat → Bool) (x : Nat) (h : p x = true) : (if p x then 1 else 2) = 1 := by
-  simp [h]
+  simp [h,]
 
 #print ex2

From 77f54e99564ecb0c50477c0c8b0bd71099cf400e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 18 Oct 2023 17:26:32 -0700
Subject: [PATCH 5/8] feat: Move list syntax to Init/Data/List/Basic

---
 src/Init/Data/List/Basic.lean | 39 ++++++++++++++++++++++++++++++++++
 src/Init/Notation.lean        | 40 -----------------------------------
 2 files changed, 39 insertions(+), 40 deletions(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index e4786a9bac2d..74e7f3ed6034 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -6,9 +6,48 @@ Author: Leonardo de Moura
 prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
+import Init.Data.Nat.Div
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
+/--
+The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
+`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
+list literals.
+
+For lists of length at least 64, an alternative desugaring strategy is used
+which uses let bindings as intermediates as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+Note that this changes the order of evaluation, although it should not be observable
+unless you use side effecting operations like `dbg_trace`.
+-/
+syntax "[" withoutPosition(term,*,?) "]"  : term
+
+/--
+Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
+The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
+It uses binary partitioning to construct a tree of intermediate let bindings as in
+`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
+-/
+syntax "%[" withoutPosition(term,*,? " | " term) "]" : term
+
+namespace Lean
+
+macro_rules
+  | `([ $elems,* ]) => do
+    -- NOTE: we do not have `TSepArray.getElems` yet at this point
+    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
+      match i, skip with
+      | 0,   _     => pure result
+      | i+1, true  => expandListLit i false result
+      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
+    let size := elems.elemsAndSeps.size
+    if size < 64 then
+      expandListLit size (size % 2 == 0) (← ``(List.nil))
+    else
+      `(%[ $elems,* | List.nil ])
+end Lean
+
 universe u v w
 
 variable {α : Type u} {β : Type v} {γ : Type w}
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 367749572632..cb6b8ed9dd11 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -460,48 +460,8 @@ expected type is known. So, `without_expected_type` is not effective in this cas
 -/
 macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
-/--
-The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
-`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
-list literals.
-
-For lists of length at least 64, an alternative desugaring strategy is used
-which uses let bindings as intermediates as in
-`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
-Note that this changes the order of evaluation, although it should not be observable
-unless you use side effecting operations like `dbg_trace`.
--/
-syntax "[" withoutPosition(term,*,?) "]"  : term
-
-/--
-Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
-The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
-It uses binary partitioning to construct a tree of intermediate let bindings as in
-`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
--/
-syntax "%[" withoutPosition(term,*,? " | " term) "]" : term
-
 namespace Lean
 
-macro_rules
-  | `([ $elems,* ]) => do
-    -- NOTE: we do not have `TSepArray.getElems` yet at this point
-    let rec isEven (i: Nat) :=
-      match i with
-      | 0 => true
-      | 1 => false
-      | i + 2 => isEven i
-    let rec expandListLit (i : Nat) (skip : Bool) (result : TSyntax `term) : MacroM Syntax := do
-      match i, skip with
-      | 0,   _     => pure result
-      | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← ``(List.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
-    let size := elems.elemsAndSeps.size
-    if size < 64 then
-      expandListLit size (isEven size) (← ``(List.nil))
-    else
-      `(%[ $elems,* | List.nil ])
-
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.

From fea24cbb08269f47dcb6cd90e5b2d7e961beb5cb Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 19 Oct 2023 19:04:57 -0700
Subject: [PATCH 6/8] refactor: Consolidate trailing comma tests

---
 tests/compiler/array.lean                  |  4 ----
 tests/compiler/array.lean.expected.out     |  1 -
 tests/lean/rewrite.lean                    |  2 +-
 tests/lean/run/simp5.lean                  |  2 +-
 tests/lean/trailingComma.lean              | 17 +++++++++++++++++
 tests/lean/trailingComma.lean.expected.out |  4 ++++
 6 files changed, 23 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/trailingComma.lean
 create mode 100644 tests/lean/trailingComma.lean.expected.out

diff --git a/tests/compiler/array.lean b/tests/compiler/array.lean
index 428c39bd385e..d0bfc5e0a8ca 100644
--- a/tests/compiler/array.lean
+++ b/tests/compiler/array.lean
@@ -11,7 +11,3 @@ def main : IO Unit := do
   IO.println (f #[2, 3, 4])
   IO.println (g #[2, 3, 4])
   IO.println (h [2, 3, 4])
-
-  -- Trailing comma
-  --IO.println (g #[5, 6, 7,])
-  IO.println (h [5, 6, 7,])
diff --git a/tests/compiler/array.lean.expected.out b/tests/compiler/array.lean.expected.out
index ec095e485b5c..04a03c85a0dd 100644
--- a/tests/compiler/array.lean.expected.out
+++ b/tests/compiler/array.lean.expected.out
@@ -1,4 +1,3 @@
 3
 [2, 3, 4]
 [2, 3, 4]
-[5, 6, 7]
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index 357055beacc6..80dc3bb54c88 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -34,7 +34,7 @@ subst y;
 exact rfl
 
 theorem ex4 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
-rewrite [appendAssoc,] at *; -- Error
+rewrite [appendAssoc] at *; -- Error
 done
 
 theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
index b7f652026051..ab7edaa8c440 100644
--- a/tests/lean/run/simp5.lean
+++ b/tests/lean/run/simp5.lean
@@ -9,6 +9,6 @@ theorem ex1 (a b c : α) : f (f a b) c = a := by
 #print ex1
 
 theorem ex2 (p : Nat → Bool) (x : Nat) (h : p x = true) : (if p x then 1 else 2) = 1 := by
-  simp [h,]
+  simp [h]
 
 #print ex2
diff --git a/tests/lean/trailingComma.lean b/tests/lean/trailingComma.lean
new file mode 100644
index 000000000000..1efad3eabc0c
--- /dev/null
+++ b/tests/lean/trailingComma.lean
@@ -0,0 +1,17 @@
+import Lean
+open Lean
+
+#eval [1,2,3,]
+#eval (2,3,)
+#eval [1,2,3,,] -- Errors, double trailing comma
+#eval (4,5,,,) -- ditto
+
+axiom zeroAdd (x : Nat) : 0 + x = x
+theorem rewrite_comma (x y z: Nat) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
+  rewrite [zeroAdd,] at *;
+  subst x;
+  subst y;
+  exact rfl
+
+theorem simp_comma (x: Nat) : x = x := by
+  simp
diff --git a/tests/lean/trailingComma.lean.expected.out b/tests/lean/trailingComma.lean.expected.out
new file mode 100644
index 000000000000..99655e890453
--- /dev/null
+++ b/tests/lean/trailingComma.lean.expected.out
@@ -0,0 +1,4 @@
+[1, 2, 3]
+(2, 3)
+trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']'
+trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')'

From 7c7e9c27dae75c1cc45b170df1ab70c3384957b6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 19 Oct 2023 21:13:28 -0700
Subject: [PATCH 7/8] test: Test the trailing comma in simp

---
 tests/lean/trailingComma.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/trailingComma.lean b/tests/lean/trailingComma.lean
index 1efad3eabc0c..380b244eedc0 100644
--- a/tests/lean/trailingComma.lean
+++ b/tests/lean/trailingComma.lean
@@ -14,4 +14,4 @@ theorem rewrite_comma (x y z: Nat) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z
   exact rfl
 
 theorem simp_comma (x: Nat) : x = x := by
-  simp
+  simp [zeroAdd,]

From f45d62052d15bd9ac8389bf9c98f672681492693 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 24 Oct 2023 00:12:37 -0700
Subject: [PATCH 8/8] test: Test invalid syntax

---
 tests/lean/StxQuot.lean              | 2 +-
 tests/lean/StxQuot.lean.expected.out | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 747c28287186..a8aa5ca3b509 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -16,7 +16,7 @@ namespace Lean.Syntax
 #eval run $ let id := miss; `($id + 1)
 end Lean.Syntax
 #eval run `(1 + 1)
-#eval run `([x,])
+#eval run `([x+])
 #eval run $ `(fun a => a) >>= pure
 #eval run $ `(def foo := 1)
 #eval run $ `(def foo := 1 def bar := 2)
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 6d637afa3006..eccd27305301 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -6,7 +6,7 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
-"(«term[_]» \"[\" [`x._@.UnhygienicMain._hyg.1 \",\"] \"]\")"
+StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"