From b6370dc929e9832a3b6dc34a324300dc86456fd2 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Thu, 26 Dec 2024 20:53:57 -0500
Subject: [PATCH] Two more indents, one failing.

---
 spec/indent_spec.lua | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/spec/indent_spec.lua b/spec/indent_spec.lua
index a13b7196..e8ce49b5 100644
--- a/spec/indent_spec.lua
+++ b/spec/indent_spec.lua
@@ -173,6 +173,42 @@ describe('indent', function()
     end)
   )
 
+  it(
+    'dedents after double indented type with braces in tactic mode',
+    helpers.clean_buffer(
+      [[
+        theorem foo :
+            bar {(n : ℤ)} = baz := by
+      ]],
+      function()
+        helpers.feed 'Gobaz'
+        assert.contents.are [[
+          theorem foo :
+              bar {(n : ℤ)} = baz := by
+            baz
+      ]]
+      end
+    )
+  )
+
+  it(
+    'dedents after double indented type with braces in term mode',
+    helpers.clean_buffer(
+      [[
+        theorem foo :
+            bar {(n : ℤ)} = baz :=
+      ]],
+      function()
+        helpers.feed 'Gobaz'
+        assert.contents.are [[
+          theorem foo :
+              bar {(n : ℤ)} = baz :=
+            baz
+      ]]
+      end
+    )
+  )
+
   it(
     'indents inside anonymous literals',
     helpers.clean_buffer(