Skip to content

Comment on Learn You an Agdaparent

Comments

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.
AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.