From 97a2198fe0f452cf951f6b002e511a70960bac15 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 18 Sep 2020 16:26:31 +0200
Subject: [PATCH] feat: change default indent width from 4 to 2 spaces

---
 src/Lean/Data/Format.lean                |  2 +-
 tests/lean/PPRoundtrip.lean.expected.out | 48 ++++++++++++------------
 2 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean
index d990bf2800..f65a5a7ff2 100644
--- a/src/Lean/Data/Format.lean
+++ b/src/Lean/Data/Format.lean
@@ -94,7 +94,7 @@ bracket "(" f ")"
 @[inline] def sbracket (f : Format) : Format :=
 bracket "[" f "]"
 
-def defIndent  := 4
+def defIndent  := 2
 def defUnicode := true
 def defWidth   := 120
 
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 1ca5a68689..4e2ea8a9de 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -16,48 +16,48 @@ id (@id Type Nat)
 fun (a : Nat) => a
 fun (a b : Nat) => a
 fun
-    (a : Nat)
-    (b : Bool) =>
-    a
+  (a : Nat)
+  (b : Bool) =>
+  a
 fun {a b : Nat} => a
 typeAs ({α : Type} → α → α) fun
-        {α :
-        Type}
-        (a : α) =>
-        a
-fun
     {α :
     Type}
-    [inst :
-    HasToString α]
     (a : α) =>
-    @toString α inst a
+    a
+fun
+  {α :
+  Type}
+  [inst :
+  HasToString α]
+  (a : α) =>
+  @toString α inst a
 (α : Type) → α
 (α β : Type) → α
 Type → Type → Type
 (α : Type) → α → α
 (α :
-    Type) →
-    (a : α) → a = a
+  Type) →
+  (a : α) → a = a
 {α : Type} → α
 {α :
-    Type} →
-    [inst :
-        HasToString α] →
-        α
+  Type} →
+  [inst :
+    HasToString α] →
+    α
 0
 1
 42
 "hi"
 {
-    type :=
-    Nat,
-    val :=
-    0 :
-    PointedType }
+  type :=
+  Nat,
+  val :=
+  0 :
+  PointedType }
 (1, 2, 3)
 (1, 2).fst
 1 < 2 || true
 id (fun
-            (a : Nat) =>
-            a) 0
+      (a : Nat) =>
+      a) 0