idris-lang/Idris-dev — pull request #1089 by david-christiansen (2014-04-20 15:33:07+00:00)
Title: Allow argument comments to span lines

Now, the following syntax is allowed:

||| @ foo docs for foo
||| more docs for foo
|||
||| @ bar docs for bar

Fixes #1024