5 ms·
That should read, "Type the following into the Emacs buffer." You should have something like: module LearnYouAn where data ℕ : Set where
by sjolsen 12y ago
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₁ = ?
- akkartik 12y agoThanks! 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.