Earlier quoted context omitted.
That should read, "Type the following into the Emacs buffer." You should have something like: module LearnYouAn where data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + m = m (succ n) + m = succ (n + m) data _even : ℕ → Set where ZERO : zero even STEP : ∀ n → n even → succ (succ n) even proof₁ : succ (succ (succ (succ (zero)))) even proof₁ = ?
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.
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
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.