From 367d61bdd540af759d9dd0117186e890c8aec6bc Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 12 Oct 2021 23:16:46 -0500
Subject: [PATCH] asdf

---
 nix/neovim.nix                               |  3 ---
 nix/nvim-agda/agda-vim-excerpts/autoload.vim | 12 +++++++++--
 nix/nvim-agda/keybinds.vim                   |  1 +
 src/plfa/part2/Lambda.lagda.md               | 22 ++++++++++++++++++--
 4 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/nix/neovim.nix b/nix/neovim.nix
index 1833a070..1b9d1424 100644
--- a/nix/neovim.nix
+++ b/nix/neovim.nix
@@ -29,9 +29,6 @@ neovim.override {
       filetype plugin indent on
       colorscheme codedark
 
-      let mapleader = ";"
-      let maplocalleader = ";"
-
       nnoremap <C-n> :NERDTreeToggle<CR>
       imap kj <Esc>
     '';
diff --git a/nix/nvim-agda/agda-vim-excerpts/autoload.vim b/nix/nvim-agda/agda-vim-excerpts/autoload.vim
index ecb7869f..48b4bc04 100644
--- a/nix/nvim-agda/agda-vim-excerpts/autoload.vim
+++ b/nix/nvim-agda/agda-vim-excerpts/autoload.vim
@@ -7,6 +7,13 @@ set cpo&vim
 if !exists('g:agda#default_glyphs')
   let g:agda#default_glyphs = {}
 
+  " Extra Shit
+  call extend(g:agda#default_glyphs, {
+    \   'Gl-': 'ƛ',
+    \   'em': '—',
+    \   '=>': '⇒',
+    \})
+
   " Combining marks
   call extend(g:agda#default_glyphs, {
     \   'over`': ' ̀',
@@ -64,10 +71,11 @@ if !exists('g:agda#default_glyphs')
     \})
 
   " Math
+    " \   ':': '∶',
   call extend(g:agda#default_glyphs, {
     \   '{{': '⦃',
     \   '}}': '⦄',
-    \   ':': '∶',
+    \   ':': '⦂',
     \   '::': '∷',
     \   ';': '﹔',
     \   '..': '‥',
@@ -87,7 +95,7 @@ if !exists('g:agda#default_glyphs')
     \   'box*': '⊠',
     \   'bul': '•',
     \   'C': 'ℂ',
-    \   'cdot': '∙',
+    \   'cdot': '·',
     \   '.': '∙',
     \   'cdots': '⋯',
     \   'check': '✓',
diff --git a/nix/nvim-agda/keybinds.vim b/nix/nvim-agda/keybinds.vim
index 6c2b7a39..7b95d35f 100644
--- a/nix/nvim-agda/keybinds.vim
+++ b/nix/nvim-agda/keybinds.vim
@@ -1,6 +1,7 @@
 nnoremap <buffer> <LocalLeader>r :<c-u>AgdaLoad<cr>
 nnoremap <buffer> <LocalLeader>t :<c-u>AgdaInfer<cr>
 nnoremap <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
+nnoremap <buffer> <LocalLeader>x :<c-u>AgdaCompute<cr>
 nnoremap <buffer> <LocalLeader>a :<c-u>AgdaRefine<cr>
 nnoremap <buffer> <LocalLeader>A :<c-u>AgdaAuto<cr>
 nnoremap <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 31bd9b23..0ab9d8f7 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -197,7 +197,11 @@ two natural numbers.  Your definition may use `plus` as
 defined earlier.
 
 ```
--- Your code goes here
+mul : Term
+mul = μ "*" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
+         case ` "m"
+           [zero⇒ ` "n"
+           |suc "m" ⇒ ` "+" · ` "n" · (` "*" · ` "m" · ` "n") ]
 ```
 
 
@@ -209,7 +213,8 @@ definition may use `plusᶜ` as defined earlier (or may not
 — there are nice definitions both ways).
 
 ```
--- Your code goes here
+mulᶜ : Term
+mulᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ (` "m" · (` "n" · ` "s") · ` "z")
 ```
 
 
@@ -262,6 +267,18 @@ plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
 ```
 Write out the definition of multiplication in the same style.
 
+```
+mul′ : Term
+mul′ = μ′ * ⇒ ƛ′ m ⇒ ƛ′ n ⇒
+          case′ m
+            [zero⇒ n
+            |suc m ⇒ plus′ · n · (* · m · n) ]
+  where
+  *  =  ` "*"
+  m  =  ` "m"
+  n  =  ` "n"
+```
+
 
 ### Formal vs informal
 
@@ -542,6 +559,7 @@ substitution.
 
 ```
 -- Your code goes here
+
 ```