feat: pretty print lists and arrays

src/Lean/Delaborator.lean

@@ -747,6 +747,27 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
 @[builtinDelab app.Not] def delabNot : Delab := delabPrefixOp fun _ x => `(¬ $x)
 @[builtinDelab app.not] def delabBNot : Delab := delabPrefixOp fun _ x => `(! $x)
 
+@[builtinDelab app.List.nil]
+def delabNil : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 1
+  `([])
+
+@[builtinDelab app.List.cons]
+def delabConsList : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 3
+  let x ← withAppFn (withAppArg delab)
+  match_syntax (← withAppArg delab) with
+  | `([])     => `([$x])
+  | `([$xs*]) => `([$x, $xs*])
+  | _         => failure
+
+@[builtinDelab app.List.toArray]
+def delabListToArray : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 2
+  match_syntax (← withAppArg delab) with
+  | `([$xs*]) => `(#[$xs*])
+  | _         => failure
+
 end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/

tests/lean/match1.lean.expected.out

@@ -31,3 +31,18 @@ fun (x : Bool × Bool) =>
 fun (x : Nat × Nat) =>
   match x with 
   | (a, b) => a + b : Nat × Nat → Nat
+fun (x x_1 : Option Nat) =>
+  match x, x_1 with 
+  | some a, some b => some (a + b)
+  | x_2, x_3 => none : Option Nat → Option Nat → Option Nat
+fun (x : Nat) =>
+  (match x with 
+    | 0 => id
+    | Nat.succ x_1 => id)
+    x : Nat → Nat
+fun (x : Array Nat) =>
+  match x with 
+  | #[1,2] => 2
+  | #[] => 0
+  | #[3,4,5] => 3
+  | x_1 => 4 : Array Nat → Nat

tests/lean/parserPrio.lean.expected.out

@@ -3,6 +3,6 @@
 parserPrio.lean:26:7: error: ambiguous, possible interpretations 
   2 * 1
   
-  1 :: List.nil
+  [1]
 sorryAx ?m : ?m
 [1, 2, 3]

tests/lean/rewrite.lean.expected.out

@@ -5,7 +5,7 @@ rewrite.lean:12:20: error: tactic 'rewrite' failed, did not find instance of the
   List.reverse (List.reverse ?m)
 α : Type _
 as bs : List α
-⊢ as ++ List.nil ++ List.nil ++ bs ++ bs = as ++ (bs ++ bs)
+⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
 x y z : Nat
 h₁ : x = y
 h₂ : y = z