akkartik on Learn You an Agda

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 11y

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.

Comments