intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Published 20 hours ago • verified publisher icon JetBrains

Equational reasoning style support in formatter

Open tonyxty opened this issue 4 years ago • 3 comments

It would be nice if the formatter could recognize equational reasoning style. Alternatively, the user could provide hints in comments specifying "this block should be formatted as equational reasoning style."

tonyxty avatar Aug 10 '20 15:08 tonyxty

I agree with OP.

ice1000 avatar Aug 10 '20 20:08 ice1000 

  ab ==< b >==
  a ==< b >==

should be formatted to

  ab ==< b >==
  a  ==< b >==

ice1000 avatar Aug 18 '20 16:08 ice1000

It might be a separate formatter?

ice1000 avatar Aug 18 '20 16:08 ice1000