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

keram · 2024-07-17T14:25:33Z

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

doc string of current function. 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: ```idris ||| Useful doc for foo foo_rhs : String -> String foo : String -> String foo str = foo_rhs str ``` After: ```idris foo_rhs : String -> String ||| Useful doc for foo foo : String -> String foo str = foo_rhs str ```

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

keram commented Jul 17, 2024

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

Are you sure you want to change the base?

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

Conversation

keram commented Jul 17, 2024

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

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