Lean Together livecoding: pin partial_fixpoint to the left in indent.

Refs: leanprover/lean4#6355
Julian · Jan 14, 2025 · b5ff076 · b5ff076
1 parent d02c5a0
commit b5ff076
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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',
   '@\\[',