naturals exercises

.gitignore

@@ -30,6 +30,7 @@ Gemfile.lock
 
 ## Emacs files
 auto/
+\#*\#
 
 ## Misc build files
 out/

emacs/init.el

@@ -1,3 +1,11 @@
+(require 'use-package)
+(require 'use-package-ensure)
+(setq use-package-always-ensure t)
+
+(use-package evil)
+(use-package agda2-mode)
+(use-package gruvbox-theme)
+
 (setq evil-undo-system 'undo-tree)
 (require 'evil)
 (evil-mode 1)

flake.nix

@@ -1,12 +1,16 @@
 {
-  inputs.nixpkgs.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
+  inputs = {
-  inputs.flake-utils.url = "github:numtide/flake-utils";
+    nixpkgs.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
-  inputs.plfa.url = "github:plfa/plfa.github.io";
+    flake-utils.url = "github:numtide/flake-utils";
-  inputs.plfa.flake = false;
+
+    plfa = {
+      flake = false;
+      url = "github:plfa/plfa.github.io";
+    };
+  };
 
   outputs = { self, nixpkgs, flake-utils, plfa }:
-    flake-utils.lib.eachDefaultSystem
+    flake-utils.lib.eachDefaultSystem (system:
-    (system:
     let
       pkgs = nixpkgs.legacyPackages.${system};
       agda = pkgs.agda.withPackages (p: [
@@ -32,17 +36,17 @@
       ]) ++ (with epkgs.elpaPackages; [
         undo-tree
       ]));
-    in {
+
-      devShell =
+    in
-        pkgs.mkShell {
+    {
-          buildInputs = [
+      devShell = pkgs.mkShell {
-            emacsWithPackages
+        buildInputs = [
-            agda
+          emacsWithPackages
-          ];
+          agda
-          shellHook = ''
+          pkgs.vscodium
-            XDG_CONFIG_HOME=$(pwd) emacs
+        ];
-          '';
+      };
-        };
+    }
-      });
+  );
-    }
+}
 

src/plfa/part1/Naturals.lagda.md

@@ -81,7 +81,7 @@ successor of two; and so on.
 Write out `7` in longhand.
 
 ```
--- Your code goes here
+_ = suc (suc (suc (suc (suc (suc (suc zero))))))
 ```
 
 
@@ -427,7 +427,8 @@ other word for evidence, which we will use interchangeably, is _proof_.
 
 #### Exercise `+-example` (practice) {name=plus-example}
 
-Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`.
+Compute `3 + 4`, writing out your reasoning as a chain of equations, using the
+equations for `+`.
 
 ```
 -- Your code goes here
@@ -506,7 +507,9 @@ Define exponentiation, which is given by the following equations:
 Check that `3 ^ 4` is `81`.
 
 ```
--- Your code goes here
+_^_ : ℕ → ℕ → ℕ
+m ^ zero = 1
+m ^ suc n = m * ( m ^ n)
 ```
 
 
@@ -919,6 +922,29 @@ Confirm that these both give the correct answer for zero through four.
 
 ```
 -- Your code goes here
+inc : Bin → Bin
+inc ⟨⟩ = ⟨⟩ O
+inc (n O) = n I
+inc (⟨⟩ I) = ⟨⟩ I O
+inc (n I) = (inc n) O
+
+_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
+_ = refl
+
+to : ℕ → Bin
+to zero = ⟨⟩ O
+to (suc n) = inc (to n)
+
+from : Bin → ℕ
+from ⟨⟩ = 0
+from (n O) = 2 * (from n)
+from (n I) = 2 * (from n) + 1
+
+_ : to 12 ≡ ⟨⟩ I I O O
+_ = refl
+
+_ : from (⟨⟩ I O I I) ≡ 11
+_ = refl
 ```