From ddf64ad7bba9331269e239ed09435f038d74463f Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Thu, 12 Dec 2024 15:24:53 -0500
Subject: [PATCH] And another.

---
 lua/lean/indent.lua                              | 16 ++++++----------
 .../indent/with_double_indented_type.in.lean     |  4 ++++
 .../indent/with_double_indented_type.lean        |  4 ++++
 3 files changed, 14 insertions(+), 10 deletions(-)
 create mode 100644 spec/fixtures/indent/with_double_indented_type.in.lean
 create mode 100644 spec/fixtures/indent/with_double_indented_type.lean

diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua
index b080da19..8f379714 100644
--- a/lua/lean/indent.lua
+++ b/lua/lean/indent.lua
@@ -69,24 +69,20 @@ function M.indentexpr(linenr)
     return shiftwidth
   elseif last_indent and focuses_at(last, last_indent + 1) then
     return last_indent + #'·'
-  elseif INDENT_AFTER:match_str(last) and not INDENT_AFTER:match_str(current) then
-    return (last_indent or 0) + shiftwidth
   elseif last_indent and is_enclosed(linenr - 1) then
     return last_indent + shiftwidth
-  elseif
-    last_indent
-    and (current_indent == 0 or math.abs(current_indent - last_indent) < shiftwidth)
-    and not is_block_comment(linenr - 2)
-  then
+  elseif current_indent and current_indent > 0 and current_indent % shiftwidth == 0 then
+    return current_indent
+  elseif last_indent and not is_block_comment(linenr - 2) then
     local dedent_one = last_indent - shiftwidth
 
     -- We could go backwards to check but that would involve looking back
     -- repetaedly over lines backwards, so we cheat and just check whether the
     -- previous line looks like it has a binder on it.
-    local is_end_of_binders = dedent_one > 0
-      and last:find '^%s*[({[]'
-      and INDENT_AFTER:match_str(current)
+    local is_end_of_binders = dedent_one > 0 and last:find '^%s*[({[]'
     return is_end_of_binders and dedent_one or last_indent
+  elseif INDENT_AFTER:match_str(last) and not INDENT_AFTER:match_str(current) then
+    return (last_indent or 0) + shiftwidth
   end
 
   return vim.fn.indent(linenr)
diff --git a/spec/fixtures/indent/with_double_indented_type.in.lean b/spec/fixtures/indent/with_double_indented_type.in.lean
new file mode 100644
index 00000000..253b25f2
--- /dev/null
+++ b/spec/fixtures/indent/with_double_indented_type.in.lean
@@ -0,0 +1,4 @@
+theorem foo
+    (hT : t = t) : t = t := by
+  have htt := hT
+  exact hT
diff --git a/spec/fixtures/indent/with_double_indented_type.lean b/spec/fixtures/indent/with_double_indented_type.lean
new file mode 100644
index 00000000..253b25f2
--- /dev/null
+++ b/spec/fixtures/indent/with_double_indented_type.lean
@@ -0,0 +1,4 @@
+theorem foo
+    (hT : t = t) : t = t := by
+  have htt := hT
+  exact hT