Pull requests: idris-hackers/idris-mode

Labels 18 Milestones 1

New pull request New

Clear current search query, filters, and sorts

5 Open 400 Closed

Author

Filter by author

Label

Filter by label

Use alt + click/return to exclude labels

or ⇧ + click/return for logical OR

Projects

Filter by project

Milestones

Filter by milestone

Reviews

Filter by reviews

No reviews Review required Approved review Changes requested

Assignee

Filter by who’s assigned

Assigned to nobody

Sort

Sort by

Newest Oldest Most commented Least commented Recently updated Least recently updated Best match

Most reactions

Pull requests list

Improve idris-filename-to-load to return expected pair of dir and relative path depending on idris-protocol version

#634 opened Jul 8, 2024 by keram

Loading…

Specify -- as comment syntax for ipkg mode

#635 opened Jul 13, 2024 by keram

Loading…

Reintroduce ipkg sourcedir regexp for Idris2 and further simplify related code.

#636 opened Jul 13, 2024 by keram • Draft

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

#637 opened Jul 17, 2024 by keram

Loading…

Make so idris-identifier-face doesn't explicitly inherit from the default face

#638 opened Oct 18, 2024 by ZharMeny

Loading…

ProTip! Type g i on any issue or pull request to go back to the issue listing page.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly