search

idris-hackers / idris-mode

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

Improve `idris-case-dwim` to make case expression from hole in edge cases #568

Closed keram closed 1 year ago

keram commented 1 year ago

when:

1) point is at ? in ?hole_rs1
Currently: Idris 1.3 errors with "Can’t make cases from ?" Idris2 does not errors but moves the point at the end of the hole 2) point is at char after ? in ?hole_rs1 Currently: Idris 1.3 errors with "funcall: example_rhs is not a pattern variable (synchronous Idris evaluation failed)") Idris2 errros with "funcall: example_rhs not defined here (synchronous Idris evaluation failed)"

Resolves: https://github.com/idris-hackers/idris-mode/issues/441

jfdm commented 1 year ago

It looks like a single workflow failed for random reasons. Re-running the job and will take it from its completion.