From b5ff076d1f201b1fb69f6f5527208d0f30ca09b9 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Tue, 14 Jan 2025 13:10:22 -0500
Subject: [PATCH] Lean Together livecoding: pin partial_fixpoint to the left in
 indent.

Refs: leanprover/lean4#6355
---
 lua/lean/indent.lua | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua
index 7747fe10..3229c6c1 100644
--- a/lua/lean/indent.lua
+++ b/lua/lean/indent.lua
@@ -20,6 +20,7 @@ local NEVER_INDENT = vim.regex(([[^\s*\(%s\)]]):format(table.concat({
   'compile_inductive% ',
   'def ',
   'instance ',
+  'partial_fixpoint',
   'structure ',
   'where',
   '@\\[',