a

.vscode/settings.json

@@ -1,4 +1,6 @@
 {
+  "editor.fontFamily": "'Roboto Mono', 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'",
+  "editor.fontSize": 15,
   "vim.insertModeKeyBindings": [
     { "before": ["k", "j"], "after": ["<Esc>"] }
   ]

flake.nix

@@ -41,7 +41,9 @@
       #   };
       # };
 
-      agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
+      neovim = pkgs.neovim;
+
+      vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
         name = "agda-mode";
         publisher = "banacorn";
         version = "0.2.19";
@@ -50,7 +52,7 @@
       combinedExtensionsDrv = pkgs.buildEnv {
         name = "vscodium-extensions";
         paths = [
-          agda-mode
+          vscode-agda-mode
           pkgs.vscode-extensions.vscodevim.vim
         ];
       };
@@ -70,6 +72,7 @@
           agda
           vscodium
           fix-whitespace
+          neovim
         ];
       };
     }

questions.txt

@@ -0,0 +1 @@
+_<_ why is one constructor allowed to only have one

src/Homework2.agda

@@ -0,0 +1,11 @@
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Data.Nat
+open import Data.Nat.Properties
+
+module Homework2 where
+
+data Bin : Set where
+  O : Bin
+  _I : Bin → Bin
+  _II : Bin → Bin

src/plfa/part1/Induction.lagda.md

@@ -891,10 +891,33 @@ Show multiplication distributes over addition, that is,
 for all naturals `m`, `n`, and `p`.
 
 ```
--- Your code goes here
 *-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
-*-distrib-+ zero n p = {! begin (zero + n) * p ≡ zero * p + n * p ∎  !}
+*-distrib-+ zero n p =
-*-distrib-+ (suc m) n p = {!   !}
+  begin
+    (zero + n) * p
+  ≡⟨ cong (_* p) (+-comm zero n) ⟩
+    (n + zero) * p
+  ≡⟨ cong (_* p) (+-identityʳ n) ⟩
+    n * p
+  ∎
+*-distrib-+ (suc m) n p =
+  begin
+    (suc m + n) * p
+  ≡⟨ cong (_* p) (+-comm (suc m) n) ⟩
+    (n + suc m) * p
+  ≡⟨ cong (_* p) (+-suc n m) ⟩
+    suc (n + m) * p
+  ≡⟨ cong (_* p) (cong suc (+-comm n m)) ⟩
+    suc (m + n) * p
+  ≡⟨⟩
+    p + (m + n) * p
+  ≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
+    p + (m * p + n * p)
+  ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
+    p + m * p + n * p
+  ≡⟨⟩
+    suc m * p + n * p
+  ∎
 ```
 
 
@@ -908,6 +931,17 @@ for all naturals `m`, `n`, and `p`.
 
 ```
 -- Your code goes here
+*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
+*-assoc zero n p =
+  begin
+    (zero * n) * p
+  ∎
+*-assoc (suc m) n p =
+  begin
+    (suc m * n) * p
+  ≡⟨  ⟩
+    
+  ∎
 ```