On my newly created emacs setup from the earlier instructions, it's not clear what "type into an emacs buffer" means. Do I create a new file with C-x C-f? Create a new buffer with C-x b? I tried both, and promptly lost agda-mode.
I then tried restarting emacs and opening a new .agda file so I get agda mode. Loaded the earlier module and then tried loading this, and it didn't seem to know about suc in the context of this buffer/file. So now I'm lost.
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₁ = ?
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 ? ?
> 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.
Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁):
On my newly created emacs setup from the earlier instructions, it's not clear what "type into an emacs buffer" means. Do I create a new file with C-x C-f? Create a new buffer with C-x b? I tried both, and promptly lost agda-mode.I then tried restarting emacs and opening a new .agda file so I get agda mode. Loaded the earlier module and then tried loading this, and it didn't seem to know about suc in the context of this buffer/file. So now I'm lost.