<div dir="ltr"><div><div><div><div><div><div><div>Let us say that we have a big agda file and we have a function at the bottom that has holes.<br></div>Whenever we case split , it takes tens of seconds to do it.<br><br></div>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.<br><br></div>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.<br><br></div>It needs to grab all the imports. It also needs to find the beginning and ending of a function.<br></div>We could use "empty" lines as the boundaries.<br><br></div>If there is code after that function, it is commented out.<br><br></div>This seems like an easy solution to me.<br></div>