idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Update `idris-make-lemma` to insert lemma above doc string of current function. #637

Open keram opened 1 month ago

keram commented 1 month ago

Why: Previously if function had a doc string the lemma was inserted before signature but after the doc string requiring user to further adjust the position.

Before:

||| Useful doc for foo
foo_rhs : String -> String

foo : String -> String
foo str = foo_rhs str

After:

foo_rhs : String -> String

||| Useful doc for foo
foo : String -> String
foo str = foo_rhs str