banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Define auto indentation rules #163

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

Defines rules for auto indenting common scenarios where the code must be indented to type check regardless. The only exception where the code doesn't strictly have to be indented is after a , but having this indentation rule makes it consistent with the behavior of ( and { and so on.

L-TChen commented 1 year ago

Can you resolve the conflicts?

fredrik-bakke commented 1 year ago

Sure thing! Give me a second

fredrik-bakke commented 1 year ago

Hold up a second, I think I spotted a mistake in one of the patterns.

fredrik-bakke commented 1 year ago

Fixed now :)

L-TChen commented 1 year ago

Thanks!