Has anyone on here implemented typed holes for any system of any kind?
There is a Shen implementation for elisp, which might the task easier compared with other platforms that have Shen ports.
Is Shen's flexibility (I have the impression that Shen can be used to implement arbitray type systems -- but this may be wrong) an obstacle to implementation of typed holes when compared to something like Idris?
The existence of proof general (although I don't know enough to use it for anything non-trivial) makes me optimistic about this question.