idris-hackers/idris-mode — pull request #151 by david-christiansen (2014-05-20 20:17:25+00:00)
Title: Make C-c C-s deal with multi-line type declarations

Now there's some heuristics to find the right place to put the added
clause in the case of definitions like

plusComm : (n, m : Nat) ->
n + m = m + n

Instead of just putting the clause on the next line, like:

plusComm : (n, m : Nat) ->
plusComm n m = ?plusComm_rhs
n + m = m + n

it finds a line that is indented the same or less than the original, producing:

plusComm : (n, m : Nat) ->
n + m = m + n
plusComm n m = ?plusComm_rhs