asdf

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>
     '';

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': '✓',

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>

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
+
 ```