Skip to content

Commit

Permalink
Two more indents, one failing.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Dec 27, 2024
1 parent 44cd9c2 commit b6370dc
Showing 1 changed file with 36 additions and 0 deletions.
36 changes: 36 additions & 0 deletions spec/indent_spec.lua
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down

0 comments on commit b6370dc

Please sign in to comment.