[Agda] Type checking times and a solution.

[Apostolis Xekoukoulotakis]

Let us say that we have a big agda file and we have a function at the
bottom that has holes.
Whenever we case split , it takes tens of seconds to do it.

Since all the previous functions are complete, one could simply create a
new file with the new function and work there. The type checking will be
instantaneous.

But this method is very tedious. An emacs command that copies the function
to another file and performs the typechecking there would be much
appreciated.

It needs to grab all the imports. It also needs to find the beginning and
ending of a function.
We could use "empty" lines as the boundaries.

If there is code after that function, it is commented out.

This seems like an easy solution to me.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170607/1659ee74/attachment.html>