2 ms·

Thanks! Can't believe I didn't think of that :/ What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for

Thanks! Can't believe I didn't think of that :/ What's the distinction between C-c C-space and C-c C-r? It looks like the former computes proof obligations for ?s, but what does the latter do? And why couldn't we use the latter in the first instance, to deduce the outermost STEP ? ? Edit: never mind, that did work.

sjolsen 12y ago
> What's the distinction between C-c C-space and C-c C-r? Beats the hell out of me. Here's the docstring for agda2-give (bound to C-c C-SPC): Give to the goal at point the expression in it Here's the one for agda2-refine (C-c C-r): Refine the goal at point. If the goal contains an expression e, and some "suffix" of the type of e unifies with the goal type, then the goal is replaced by e applied to a suitable number of new goals. If the goal is empty, the goal type is a data type, and there is exactly one constructor which unifies with this type, then the goal is replaced by the constructor applied to a suitable number of new goals.