4 ms·

It lost me at this point: Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁): proof₁ : suc (suc (suc (s

It lost me at this point: Type the following into an emacs buffer, and then type C-c C-l (use \_1 to type the subscript symbol ₁): proof₁ : suc (suc (suc (suc zero))) even proof₁ = ? 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.

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 ago
  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 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.

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 ago
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 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.