Closed carl-westerlund closed 1 year ago
I'm quite new to Lean so I'm sorry if I have misunderstood something, but shouldn't tactics inside curly bracket blocks also be highlighted? If I change the curly brackets to begin ... end it works.
begin ... end
This was apparently caused by another plugin.
I'm quite new to Lean so I'm sorry if I have misunderstood something, but shouldn't tactics inside curly bracket blocks also be highlighted? If I change the curly brackets to
begin ... end
it works.