Compare commits
28 commits
Author | Date | ||
---|---|---|---|
cb8431dbcc | |||
fbc44a0f78 | |||
8c4fe03730 | |||
d24d992786 | |||
367d61bdd5 | |||
bc087ff31e | |||
dcb4cbb360 | |||
7dff3e17e8 | |||
0eec924486 | |||
7149274cf4 | |||
87fafc7a15 | |||
8b1fbba12a | |||
658bd841f0 | |||
8d0bebab0b | |||
fceaaa8f83 | |||
32ed3d6920 | |||
93f496e3c0 | |||
bf178e1b8b | |||
3830722f67 | |||
583e0fb344 | |||
00ec52d94a | |||
|
84840b0d4d | ||
|
efd14e775f | ||
|
9dc763832f | ||
|
b6700e732c | ||
|
c2c3cce920 | ||
|
0c7bf0508a | ||
|
61b2259d99 |
32 changed files with 2128 additions and 12 deletions
9
.envrc
Normal file
9
.envrc
Normal file
|
@ -0,0 +1,9 @@
|
|||
use_flake() {
|
||||
watch_file flake.nix
|
||||
watch_file flake.lock
|
||||
eval "$(nix print-dev-env --profile "$(direnv_layout_dir)/flake-profile")"
|
||||
}
|
||||
|
||||
mkdir -p .direnv
|
||||
|
||||
use_flake
|
1
.gitignore
vendored
1
.gitignore
vendored
|
@ -30,6 +30,7 @@ Gemfile.lock
|
|||
|
||||
## Emacs files
|
||||
auto/
|
||||
\#*\#
|
||||
|
||||
## Misc build files
|
||||
out/
|
||||
|
|
2
.gitmodules
vendored
2
.gitmodules
vendored
|
@ -1,3 +1,3 @@
|
|||
[submodule "standard-library"]
|
||||
path = standard-library
|
||||
url = git@github.com:agda/agda-stdlib.git
|
||||
url = https://github.com/agda/agda-stdlib.git
|
||||
|
|
7
.vscode/settings.json
vendored
Normal file
7
.vscode/settings.json
vendored
Normal file
|
@ -0,0 +1,7 @@
|
|||
{
|
||||
"editor.fontSize": 15,
|
||||
"vim.insertModeKeyBindings": [
|
||||
{ "before": ["k", "j"], "after": ["<Esc>"] }
|
||||
],
|
||||
"editor.fontFamily": "\"PragmataPro Mono Liga\", \"Roboto Mono\", 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'"
|
||||
}
|
|
@ -101,7 +101,7 @@ PLFA ships with the required version of the Agda standard library, so if you clo
|
|||
If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that!
|
||||
```bash
|
||||
cd plfa/
|
||||
git submodule update --recursive
|
||||
git submodule update --init --recursive
|
||||
```
|
||||
If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]:
|
||||
```bash
|
||||
|
|
26
emacs/init.el
Normal file
26
emacs/init.el
Normal file
|
@ -0,0 +1,26 @@
|
|||
(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)
|
||||
|
||||
(load-theme 'gruvbox t)
|
||||
|
||||
(menu-bar-mode -1)
|
||||
(tool-bar-mode -1)
|
||||
(toggle-scroll-bar -1)
|
||||
|
||||
(load-file (let ((coding-system-for-read 'utf-8))
|
||||
(shell-command-to-string "agda-mode locate")))
|
||||
|
||||
(setq auto-mode-alist
|
||||
(append
|
||||
'(("\\.agda\\'" . agda2-mode)
|
||||
("\\.lagda.md\\'" . agda2-mode))
|
||||
auto-mode-alist))
|
77
flake.lock
Normal file
77
flake.lock
Normal file
|
@ -0,0 +1,77 @@
|
|||
{
|
||||
"nodes": {
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1631561581,
|
||||
"narHash": "sha256-3VQMV5zvxaVLvqqUrNz3iJelLw30mIVSfZmAaauM3dA=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "7e5bf3925f6fbdfaf50a2a7ca0be2879c4261d19",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1634090417,
|
||||
"narHash": "sha256-GGRQSC+dBFtynnwHCG65bdzygXK058NJ92boHGXz8Gg=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "c9ddb803ce95c0ec2ab4d57ba29f136b8ce9fe71",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-agda": {
|
||||
"locked": {
|
||||
"lastModified": 1624913309,
|
||||
"narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "860b56be91fb874d48e23a950815969a7b832fbc",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "860b56be91fb874d48e23a950815969a7b832fbc",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"plfa": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1628614312,
|
||||
"narHash": "sha256-e5wLKKjabrZesjAd5p5sXeYW28LXoZPGY2jp6cnB9qM=",
|
||||
"owner": "plfa",
|
||||
"repo": "plfa.github.io",
|
||||
"rev": "8fec0eb208e48401908414347d060767af48309f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "plfa",
|
||||
"repo": "plfa.github.io",
|
||||
"rev": "8fec0eb208e48401908414347d060767af48309f",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-agda": "nixpkgs-agda",
|
||||
"plfa": "plfa"
|
||||
}
|
||||
}
|
||||
},
|
||||
"root": "root",
|
||||
"version": 7
|
||||
}
|
69
flake.nix
Normal file
69
flake.nix
Normal file
|
@ -0,0 +1,69 @@
|
|||
{
|
||||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs";
|
||||
flake-utils.url = "github:numtide/flake-utils";
|
||||
|
||||
nixpkgs-agda.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
|
||||
plfa = {
|
||||
flake = false;
|
||||
url = "github:plfa/plfa.github.io?rev=8fec0eb208e48401908414347d060767af48309f";
|
||||
};
|
||||
};
|
||||
|
||||
outputs = { self, nixpkgs, nixpkgs-agda, flake-utils, plfa }:
|
||||
flake-utils.lib.eachDefaultSystem (system:
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
|
||||
myPkgs = rec {
|
||||
agda = import ./nix/agda.nix {
|
||||
inherit system plfa;
|
||||
nixpkgs = nixpkgs-agda;
|
||||
};
|
||||
nvim-agda = import ./nix/nvim-agda {
|
||||
inherit system;
|
||||
nixpkgs = nixpkgs-agda;
|
||||
};
|
||||
|
||||
neovim = pkgs.callPackage ./nix/neovim.nix { inherit nvim-agda; };
|
||||
};
|
||||
|
||||
vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
|
||||
name = "agda-mode";
|
||||
publisher = "banacorn";
|
||||
version = "0.2.19";
|
||||
sha256 = "2PFfFySOoxFEZdYb2BF6XQeYEygbTn/WJub/8IKfc1Y=";
|
||||
};
|
||||
combinedExtensionsDrv = pkgs.buildEnv {
|
||||
name = "vscodium-extensions";
|
||||
paths = [
|
||||
vscode-agda-mode
|
||||
pkgs.vscode-extensions.vscodevim.vim
|
||||
];
|
||||
};
|
||||
vscodium = pkgs.runCommand "vscodium-with-extensions" {
|
||||
nativeBuildInputs = [ pkgs.makeWrapper ];
|
||||
buildInputs = [ pkgs.vscodium ];
|
||||
meta = pkgs.vscodium.meta;
|
||||
} ''
|
||||
mkdir -p $out/bin
|
||||
makeWrapper "${pkgs.vscodium}/bin/codium" "$out/bin/codium" \
|
||||
--add-flags "--extensions-dir ${combinedExtensionsDrv}/share/vscode/extensions"
|
||||
'';
|
||||
in
|
||||
{
|
||||
packages = flake-utils.lib.flattenTree myPkgs;
|
||||
|
||||
devShell = pkgs.mkShell {
|
||||
buildInputs = with pkgs; with myPkgs; [
|
||||
agda
|
||||
vscodium
|
||||
neovim
|
||||
nvim-agda
|
||||
lua51Packages.luautf8
|
||||
];
|
||||
};
|
||||
}
|
||||
);
|
||||
}
|
||||
|
20
nix/agda.nix
Normal file
20
nix/agda.nix
Normal file
|
@ -0,0 +1,20 @@
|
|||
{ nixpkgs, system, plfa, ... }:
|
||||
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
in
|
||||
pkgs.agda.withPackages (p: [
|
||||
p.standard-library
|
||||
(p.mkDerivation {
|
||||
pname = "plfa";
|
||||
meta = null;
|
||||
version = "1.0.0";
|
||||
buildInputs = [ p.standard-library ];
|
||||
preBuild = ''
|
||||
echo "module Everything where" > Everything.agda
|
||||
find src -name '*.lagda.md' | sed -e 's/src\///' -e 's/\.lagda\.md//' -e 's/\//\./g' -e 's/^/import /' | grep -Ev '^import plfa\.part1\.Equality|Naturals$' >> Everything.agda
|
||||
export LANG=C.UTF-8
|
||||
'';
|
||||
src = plfa;
|
||||
})
|
||||
])
|
36
nix/neovim.nix
Normal file
36
nix/neovim.nix
Normal file
|
@ -0,0 +1,36 @@
|
|||
{ neovim, vimPlugins, luajitPackages, nvim-agda }:
|
||||
|
||||
neovim.override {
|
||||
configure = {
|
||||
plug = {
|
||||
plugins = with vimPlugins; [
|
||||
ctrlp-vim
|
||||
nerdtree
|
||||
nvim-agda
|
||||
vim-code-dark
|
||||
vim-polyglot
|
||||
];
|
||||
};
|
||||
|
||||
customRC = ''
|
||||
lua << EOF
|
||||
package.cpath = package.cpath .. ";${luajitPackages.luautf8}/lib/lua/5.1/lua-utf8.so"
|
||||
EOF
|
||||
|
||||
set hidden
|
||||
set cursorline
|
||||
set number
|
||||
set splitright
|
||||
set modeline
|
||||
set expandtab
|
||||
set colorcolumn=80
|
||||
syntax on
|
||||
filetype on
|
||||
filetype plugin indent on
|
||||
colorscheme codedark
|
||||
|
||||
nnoremap <C-n> :NERDTreeToggle<CR>
|
||||
imap kj <Esc>
|
||||
'';
|
||||
};
|
||||
}
|
24
nix/nvim-agda/agda-vim-excerpts/LICENSE
Normal file
24
nix/nvim-agda/agda-vim-excerpts/LICENSE
Normal file
|
@ -0,0 +1,24 @@
|
|||
Copyright (c) 2013, Derek Elkins
|
||||
All rights reserved.
|
||||
|
||||
Redistribution and use in source and binary forms, with or without
|
||||
modification, are permitted provided that the following conditions are met:
|
||||
|
||||
Redistributions of source code must retain the above copyright notice, this
|
||||
list of conditions and the following disclaimer.
|
||||
|
||||
Redistributions in binary form must reproduce the above copyright
|
||||
notice, this list of conditions and the following disclaimer in the
|
||||
documentation and/or other materials provided with the distribution.
|
||||
|
||||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
|
||||
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
|
||||
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
|
||||
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
2
nix/nvim-agda/agda-vim-excerpts/README
Normal file
2
nix/nvim-agda/agda-vim-excerpts/README
Normal file
|
@ -0,0 +1,2 @@
|
|||
autoload.vim and ftplugin.vim are mostly taken from
|
||||
https://github.com/derekelkins/agda-vim, with slight modification.
|
668
nix/nvim-agda/agda-vim-excerpts/autoload.vim
Normal file
668
nix/nvim-agda/agda-vim-excerpts/autoload.vim
Normal file
|
@ -0,0 +1,668 @@
|
|||
" Agda Input Abbreviations
|
||||
"
|
||||
let s:cpo_save = &cpo
|
||||
set cpo&vim
|
||||
|
||||
" Public to allow referencing in custom overrides.
|
||||
if !exists('g:agda#default_glyphs')
|
||||
let g:agda#default_glyphs = {}
|
||||
|
||||
" Extra Shit
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'Gl-': 'ƛ',
|
||||
\ '==': '≡',
|
||||
\ '<': '⟨',
|
||||
\ '>': '⟩',
|
||||
\ 'em': '—',
|
||||
\ '=>': '⇒',
|
||||
\ '~-': '≃',
|
||||
\ 'r': '→',
|
||||
\ '0': '∅',
|
||||
\})
|
||||
|
||||
" Combining marks
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'over`': ' ̀',
|
||||
\ "over'": ' ́',
|
||||
\ 'over^': ' ̂',
|
||||
\ 'overv': ' ̌',
|
||||
\ 'over~': ' ̃',
|
||||
\ 'over-': ' ̄',
|
||||
\ 'over_': ' ̅',
|
||||
\ 'over–': ' ̅',
|
||||
\ 'over—': ' ̅',
|
||||
\ 'overcup': ' ̆',
|
||||
\ 'overcap': ' ̑',
|
||||
\ 'over.': ' ̇',
|
||||
\ 'over..': ' ̈',
|
||||
\ 'over"': ' ̈',
|
||||
\ 'over...': ' ⃛',
|
||||
\ 'overright.': ' ͘',
|
||||
\ 'overo': ' ̊',
|
||||
\ 'over``': ' ̏',
|
||||
\ "over''": ' ̋',
|
||||
\ 'overvec': ' ⃑',
|
||||
\ 'vec': ' ⃑',
|
||||
\ 'overlvec': ' ⃐',
|
||||
\ 'lvec': ' ⃐',
|
||||
\ 'overarc': ' ⃕',
|
||||
\ 'overlarc': ' ⃔',
|
||||
\ 'overto': ' ⃗',
|
||||
\ 'overfrom': ' ⃖',
|
||||
\ 'overfromto': ' ⃡',
|
||||
\ 'over*': ' ⃰',
|
||||
\ 'under`': ' ̖',
|
||||
\ "under'": ' ̗',
|
||||
\ 'under,': ' ̗',
|
||||
\ 'under.': ' ̣',
|
||||
\ 'under..': ' ̤',
|
||||
\ 'under"': ' ̤',
|
||||
\ 'undero': ' ̥',
|
||||
\ 'under-': ' ̱',
|
||||
\ 'under_': ' ̲',
|
||||
\ 'under–': ' ̲',
|
||||
\ 'under—': ' ̲',
|
||||
\ 'through~': ' ̴',
|
||||
\ 'through-': ' ̵',
|
||||
\ 'through_': ' ̶',
|
||||
\ 'through–': ' ̶',
|
||||
\ 'through—': ' ̶',
|
||||
\ 'through/': ' ̷',
|
||||
\ 'not': ' ̷',
|
||||
\ 'through?': ' ̸',
|
||||
\ 'Not': ' ̸',
|
||||
\ 'through\|': ' ⃒',
|
||||
\ 'throughshortmid': ' ⃓',
|
||||
\ 'througho': ' ⃘',
|
||||
\})
|
||||
|
||||
" Math
|
||||
" \ ':': '∶',
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '{{': '⦃',
|
||||
\ '}}': '⦄',
|
||||
\ ':': '⦂',
|
||||
\ '::': '∷',
|
||||
\ ';': '﹔',
|
||||
\ '..': '‥',
|
||||
\ '=?': '≟',
|
||||
\ 'all': '∀',
|
||||
\ 'always': '□',
|
||||
\ 'approx': '≈',
|
||||
\ 'bot': '⊥',
|
||||
\ 'box': '□',
|
||||
\ 'boxdot': '⊡',
|
||||
\ 'box.': '⊡',
|
||||
\ 'boxminus': '⊟',
|
||||
\ 'box-': '⊟',
|
||||
\ 'boxplus': '⊞',
|
||||
\ 'box+': '⊞',
|
||||
\ 'boxtimes': '⊠',
|
||||
\ 'box*': '⊠',
|
||||
\ 'bul': '•',
|
||||
\ 'C': 'ℂ',
|
||||
\ 'cdot': '·',
|
||||
\ '.': '∙',
|
||||
\ 'cdots': '⋯',
|
||||
\ 'check': '✓',
|
||||
\ 'yes': '✓',
|
||||
\ 'Check': '✔',
|
||||
\ 'Yes': '✔',
|
||||
\ 'circ': '∘',
|
||||
\ 'clock': '↻',
|
||||
\ 'cclock': '↺',
|
||||
\ 'comp': '∘',
|
||||
\ 'contra': '↯',
|
||||
\ 'deg': '°',
|
||||
\ 'den': '⟦⟧<left>',
|
||||
\ 'diamond': '◇',
|
||||
\ 'dots': '…',
|
||||
\ 'down': '↓',
|
||||
\ 'downtri': '▼',
|
||||
\ 'Down': '⇓',
|
||||
\ 'dunion': '⊎',
|
||||
\ 'du': '⊎',
|
||||
\ 'ell': 'ℓ',
|
||||
\ 'empty': '∅',
|
||||
\ 'equiv': '≡',
|
||||
\ 'eq': '≡',
|
||||
\ 'eventually': '◇',
|
||||
\ 'exists': '∃',
|
||||
\ 'flat': '♭',
|
||||
\ 'fold': '⦇⦈<left>',
|
||||
\ '(\|': '⦇',
|
||||
\ '\|)': '⦈',
|
||||
\ 'forall': '∀',
|
||||
\ 'from': '←',
|
||||
\ '<-': '←',
|
||||
\ 'From': '⇐',
|
||||
\ 'fromto': '↔',
|
||||
\ 'Fromto': '⇔',
|
||||
\ 'ge': '≥',
|
||||
\ 'glub': '⊓',
|
||||
\ 'iff': '⇔',
|
||||
\ 'implies': '⇒',
|
||||
\ 'impliedby': '⇐',
|
||||
\ 'in': '∈',
|
||||
\ 'infty': '∞',
|
||||
\ 'inf': '∞',
|
||||
\ 'int': '∫',
|
||||
\ 'intersect': '∩',
|
||||
\ 'iso': '≅',
|
||||
\ 'join': '⋈',
|
||||
\ 'land': '∧',
|
||||
\ 'langle': '⟨',
|
||||
\ 'lbrac': '⟦',
|
||||
\ '[[': '⟦',
|
||||
\ 'ldots': '…',
|
||||
\ 'ldown': '⇃',
|
||||
\ 'leadsto': '⇝',
|
||||
\ '~>': '⇝',
|
||||
\ 'le': '≤',
|
||||
\ 'lift': '⌊⌋<left>',
|
||||
\ 'floor': '⌊⌋<left>',
|
||||
\ 'llangle': '⟪',
|
||||
\ 'longto': '⟶ ',
|
||||
\ '--': '⟶ ',
|
||||
\ '–': '⟶ ',
|
||||
\ 'lor': '∨',
|
||||
\ 'lower': '⌈⌉<left>',
|
||||
\ 'ceil': '⌈⌉<left>',
|
||||
\ 'lub': '⊔',
|
||||
\ 'lup': '↿',
|
||||
\ 'mapsto': '↦',
|
||||
\ 'map': '↦',
|
||||
\ 'mid': '∣',
|
||||
\ 'models': '⊨',
|
||||
\ '\|=': '⊨',
|
||||
\ 'N': 'ℕ',
|
||||
\ 'ne': '≠',
|
||||
\ 'nearrow': '↗',
|
||||
\ 'Nearrow': '⇗',
|
||||
\ 'neg': '¬',
|
||||
\ '/=': '≠',
|
||||
\ 'nequiv': '≢',
|
||||
\ 'neq': '≢',
|
||||
\ 'nexist': '∄',
|
||||
\ 'none': '∄',
|
||||
\ 'ni': '∋',
|
||||
\ 'nin': '∉',
|
||||
\ 'niso': '≇',
|
||||
\ 'notin': '∉',
|
||||
\ 'nwarrow': '↖',
|
||||
\ 'Nwarrow': '⇖',
|
||||
\ 'oast': '⊛',
|
||||
\ 'odot': '⊙',
|
||||
\ 'o.': '⊙',
|
||||
\ 'of': '∘',
|
||||
\ 'o': '∘',
|
||||
\ 'ominus': '⊖',
|
||||
\ 'o-': '⊖',
|
||||
\ 'oplus': '⊕',
|
||||
\ 'o+': '⊕',
|
||||
\ 'oslash': '⊘',
|
||||
\ 'o/': '⊘',
|
||||
\ 'otimes': '⊗',
|
||||
\ 'o*': '⊗',
|
||||
\ 'par': '∂',
|
||||
\ 'pge': '≽',
|
||||
\ 'pgt': '≻',
|
||||
\ 'ple': '≼',
|
||||
\ 'plt': '≺',
|
||||
\ 'p≥': '≽',
|
||||
\ 'p>': '≻',
|
||||
\ 'p≤': '≼',
|
||||
\ 'p<': '≺',
|
||||
\ 'pm': '±',
|
||||
\ 'prec': '≼',
|
||||
\ 'prod': '∏',
|
||||
\ 'proves': '⊢',
|
||||
\ '\|-': '⊢',
|
||||
\ 'provedby': '⊣',
|
||||
\ 'Q': 'ℚ',
|
||||
\ 'qed': '∎',
|
||||
\ 'R': 'ℝ',
|
||||
\ 'rangle': '⟩',
|
||||
\ 'rbrac': '⟧',
|
||||
\ ']]': '⟧',
|
||||
\ 'rdown': '⇂',
|
||||
\ 'righttri': '▸',
|
||||
\ 'rrangle': '⟫',
|
||||
\ 'rup': '↾',
|
||||
\ 'searrow': '↘',
|
||||
\ 'Searrow': '⇘',
|
||||
\ 'setminus': '∖',
|
||||
\ 'sharp': '♯',
|
||||
\ '#': '♯',
|
||||
\ 'sim': '∼',
|
||||
\ 'simeq': '≃',
|
||||
\ 'some': '∃',
|
||||
\ 'sqge': '⊒',
|
||||
\ 'sqgt': '⊐',
|
||||
\ 'sqle': '⊑',
|
||||
\ 'sqlt': '⊏',
|
||||
\ 's≥': '⊒',
|
||||
\ 's>': '⊐',
|
||||
\ 's≤': '⊑',
|
||||
\ 's<': '⊏',
|
||||
\ 'sqr': '²',
|
||||
\ 'sqrt': '√',
|
||||
\ 'star': '✭',
|
||||
\ 'subset': '⊂',
|
||||
\ 'sub': '⊂',
|
||||
\ 'subseteq': '⊆',
|
||||
\ 'subeq': '⊆',
|
||||
\ 'subsetneq': '⊊',
|
||||
\ 'subneq': '⊊',
|
||||
\ 'sum': '∑',
|
||||
\ 'supset': '⊃',
|
||||
\ 'sup': '⊃',
|
||||
\ 'supseteq': '⊇',
|
||||
\ 'supeq': '⊇',
|
||||
\ 'supsetneq': '⊋',
|
||||
\ 'supneq': '⊋',
|
||||
\ 'swarrow': '↙',
|
||||
\ 'Swarrow': '⇙',
|
||||
\ 'thus': '∴',
|
||||
\ 'times': '×',
|
||||
\ '*': '×',
|
||||
\ 'to': '→',
|
||||
\ '-': '→',
|
||||
\ 'To': '⇒',
|
||||
\ '=': '⇒',
|
||||
\ 'top': '⊤',
|
||||
\ 'tuple': '⟨⟩<left>',
|
||||
\ 'up': '↑',
|
||||
\ 'updown': '↕',
|
||||
\ 'ud': '↕',
|
||||
\ 'unfold': '⦉⦊<left>',
|
||||
\ '<\|': '⦉',
|
||||
\ '\|>': '⦊',
|
||||
\ 'up;down': '⇅',
|
||||
\ 'u;d': '⇅',
|
||||
\ 'uptri': '▲',
|
||||
\ 'Up': '⇑',
|
||||
\ 'union': '∪',
|
||||
\ 'vdots': '⋮',
|
||||
\ 'voltage': '⚡',
|
||||
\ 'xmark': '✗',
|
||||
\ 'no': '✗',
|
||||
\ 'Xmark': '✘',
|
||||
\ 'No': '✘',
|
||||
\ 'Z': 'ℤ',
|
||||
\})
|
||||
|
||||
" Not math
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'sec': '§',
|
||||
\})
|
||||
|
||||
" Superscripts
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '^0': '⁰',
|
||||
\ '^1': '¹',
|
||||
\ '^2': '²',
|
||||
\ '^3': '³',
|
||||
\ '^4': '⁴',
|
||||
\ '^5': '⁵',
|
||||
\ '^6': '⁶',
|
||||
\ '^7': '⁷',
|
||||
\ '^8': '⁸',
|
||||
\ '^9': '⁹',
|
||||
\ '^A': 'ᴬ',
|
||||
\ '^B': 'ᴮ',
|
||||
\ '^D': 'ᴰ',
|
||||
\ '^E': 'ᴱ',
|
||||
\ '^G': 'ᴳ',
|
||||
\ '^H': 'ᴴ',
|
||||
\ '^I': 'ᴵ',
|
||||
\ '^J': 'ᴶ',
|
||||
\ '^K': 'ᴷ',
|
||||
\ '^L': 'ᴸ',
|
||||
\ '^M': 'ᴹ',
|
||||
\ '^N': 'ᴺ',
|
||||
\ '^O': 'ᴼ',
|
||||
\ '^P': 'ᴾ',
|
||||
\ '^R': 'ᴿ',
|
||||
\ '^T': 'ᵀ',
|
||||
\ '^U': 'ᵁ',
|
||||
\ '^V': 'ⱽ',
|
||||
\ '^W': 'ᵂ',
|
||||
\ '^a': 'ᵃ',
|
||||
\ '^b': 'ᵇ',
|
||||
\ '^c': 'ᶜ',
|
||||
\ '^d': 'ᵈ',
|
||||
\ '^e': 'ᵉ',
|
||||
\ '^f': 'ᶠ',
|
||||
\ '^g': 'ᵍ',
|
||||
\ '^h': 'ʰ',
|
||||
\ '^i': 'ⁱ',
|
||||
\ '^j': 'ʲ',
|
||||
\ '^k': 'ᵏ',
|
||||
\ '^l': 'ˡ',
|
||||
\ '^m': 'ᵐ',
|
||||
\ '^n': 'ⁿ',
|
||||
\ '^o': 'ᵒ',
|
||||
\ '^p': 'ᵖ',
|
||||
\ '^r': 'ʳ',
|
||||
\ '^s': 'ˢ',
|
||||
\ '^t': 'ᵗ',
|
||||
\ '^u': 'ᵘ',
|
||||
\ '^v': 'ᵛ',
|
||||
\ '^w': 'ʷ',
|
||||
\ '^x': 'ˣ',
|
||||
\ '^y': 'ʸ',
|
||||
\ '^z': 'ᶻ',
|
||||
\ '^+': '⁺',
|
||||
\ '^-': '⁻',
|
||||
\ '^=': '⁼',
|
||||
\ '^(': '⁽',
|
||||
\ '^)': '⁾',
|
||||
\ "'": '′',
|
||||
\ "''": '″',
|
||||
\ "'''": '‴',
|
||||
\ "''''": '⁗',
|
||||
\ '"': '″',
|
||||
\ '""': '⁗',
|
||||
\ '`': '‵',
|
||||
\ '``': '‶',
|
||||
\ '```': '‷',
|
||||
\})
|
||||
|
||||
" Subscripts
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '_0': '₀',
|
||||
\ '_1': '₁',
|
||||
\ '_2': '₂',
|
||||
\ '_3': '₃',
|
||||
\ '_4': '₄',
|
||||
\ '_5': '₅',
|
||||
\ '_6': '₆',
|
||||
\ '_7': '₇',
|
||||
\ '_8': '₈',
|
||||
\ '_9': '₉',
|
||||
\ '_a': 'ₐ',
|
||||
\ '_e': 'ₑ',
|
||||
\ '_h': 'ₕ',
|
||||
\ '_i': 'ᵢ',
|
||||
\ '_j': 'ⱼ',
|
||||
\ '_k': 'ₖ',
|
||||
\ '_l': 'ₗ',
|
||||
\ '_m': 'ₘ',
|
||||
\ '_n': 'ₙ',
|
||||
\ '_o': 'ₒ',
|
||||
\ '_p': 'ₚ',
|
||||
\ '_r': 'ᵣ',
|
||||
\ '_s': 'ₛ',
|
||||
\ '_t': 'ₜ',
|
||||
\ '_u': 'ᵤ',
|
||||
\ '_v': 'ᵥ',
|
||||
\ '_x': 'ₓ',
|
||||
\ '_+': '₊',
|
||||
\ '_-': '₋',
|
||||
\ '_=': '₌',
|
||||
\ '_(': '₍',
|
||||
\ '_)': '₎',
|
||||
\ 'p0': 'π₀',
|
||||
\ 'p1': 'π₁',
|
||||
\ 'p2': 'π₂',
|
||||
\ 'p3': 'π₃',
|
||||
\ 'p4': 'π₄',
|
||||
\ 'p5': 'π₅',
|
||||
\ 'p6': 'π₆',
|
||||
\ 'p7': 'π₇',
|
||||
\ 'p8': 'π₈',
|
||||
\ 'p9': 'π₉',
|
||||
\ 'i0': 'ι₀',
|
||||
\ 'i1': 'ι₁',
|
||||
\ 'i2': 'ι₂',
|
||||
\ 'i3': 'ι₃',
|
||||
\ 'i4': 'ι₄',
|
||||
\ 'i5': 'ι₅',
|
||||
\ 'i6': 'ι₆',
|
||||
\ 'i7': 'ι₇',
|
||||
\ 'i8': 'ι₈',
|
||||
\ 'i9': 'ι₉',
|
||||
\})
|
||||
|
||||
" Greek (lower)
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'alpha': 'α',
|
||||
\ 'a': 'α',
|
||||
\ 'beta': 'β',
|
||||
\ 'b': 'β',
|
||||
\ 'gamma': 'γ',
|
||||
\ 'g': 'γ',
|
||||
\ 'delta': 'δ',
|
||||
\ 'd': 'δ',
|
||||
\ 'epsilon': 'ε',
|
||||
\ 'e': 'ε',
|
||||
\ 'zeta': 'ζ',
|
||||
\ 'z': 'ζ',
|
||||
\ 'eta': 'η',
|
||||
\ 'h': 'η',
|
||||
\ 'theta': 'θ',
|
||||
\ 'iota': 'ι',
|
||||
\ 'i': 'ι',
|
||||
\ 'kappa': 'κ',
|
||||
\ 'k': 'κ',
|
||||
\ 'lambda': 'λ',
|
||||
\ 'l': 'λ',
|
||||
\ 'mu': 'μ',
|
||||
\ 'm': 'μ',
|
||||
\ 'nu': 'ν',
|
||||
\ 'n': 'ν',
|
||||
\ 'xi': 'ξ',
|
||||
\ 'omicron': 'ο',
|
||||
\ 'pi': 'π',
|
||||
\ 'p': 'π',
|
||||
\ 'rho': 'ρ',
|
||||
\ 'sigma': 'σ',
|
||||
\ 's': 'σ',
|
||||
\ 'varsigma': 'ς',
|
||||
\ 'vars': 'ς',
|
||||
\ 'tau': 'τ',
|
||||
\ 't': 'τ',
|
||||
\ 'u': 'υ',
|
||||
\ 'phi': 'φ',
|
||||
\ 'f': 'φ',
|
||||
\ 'chi': 'χ',
|
||||
\ 'x': 'χ',
|
||||
\ 'psi': 'ψ',
|
||||
\ 'c': 'ψ',
|
||||
\ 'omega': 'ω',
|
||||
\ 'v': 'ω',
|
||||
\})
|
||||
|
||||
" Greek (upper)
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'Alpha': 'Α',
|
||||
\ 'Beta': 'Β',
|
||||
\ 'Gamma': 'Γ',
|
||||
\ 'G': 'Γ',
|
||||
\ 'Delta': 'Δ',
|
||||
\ 'D': 'Δ',
|
||||
\ 'Epsilon': 'Ε',
|
||||
\ 'Zeta': 'Ζ',
|
||||
\ 'Eta': 'Η',
|
||||
\ 'Theta': 'Θ',
|
||||
\ 'Iota': 'Ι',
|
||||
\ 'Kappa': 'Κ',
|
||||
\ 'Lambda': 'Λ',
|
||||
\ 'L': 'Λ',
|
||||
\ 'Mu': 'Μ',
|
||||
\ 'Nu': 'Ν',
|
||||
\ 'Xi': 'Ξ',
|
||||
\ 'Omicron': 'Ο',
|
||||
\ 'Pi': 'Π',
|
||||
\ 'P': 'Π',
|
||||
\ 'Rho': 'Ρ',
|
||||
\ 'Sigma': 'Σ',
|
||||
\ 'S': 'Σ',
|
||||
\ 'Tau': 'Τ',
|
||||
\ 'Upsilon': 'Υ',
|
||||
\ 'Phi': 'Φ',
|
||||
\ 'F': 'Φ',
|
||||
\ 'Chi': 'Χ',
|
||||
\ 'Psi': 'Ψ',
|
||||
\ 'Omega': 'Ω',
|
||||
\ 'V': 'Ω',
|
||||
\})
|
||||
|
||||
" Blackboard
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'bA': '𝔸',
|
||||
\ 'bB': '𝔹',
|
||||
\ 'bC': 'ℂ',
|
||||
\ 'bD': '𝔻',
|
||||
\ 'bE': '𝔼',
|
||||
\ 'bF': '𝔽',
|
||||
\ 'bG': '𝔾',
|
||||
\ 'bH': 'ℍ',
|
||||
\ 'bI': '𝕀',
|
||||
\ 'bJ': '𝕁',
|
||||
\ 'bK': '𝕂',
|
||||
\ 'bL': '𝕃',
|
||||
\ 'bM': '𝕄',
|
||||
\ 'bN': 'ℕ',
|
||||
\ 'bO': '𝕆',
|
||||
\ 'bP': 'ℙ',
|
||||
\ 'bQ': 'ℚ',
|
||||
\ 'bR': 'ℝ',
|
||||
\ 'bS': '𝕊',
|
||||
\ 'bT': '𝕋',
|
||||
\ 'bU': '𝕌',
|
||||
\ 'bV': '𝕍',
|
||||
\ 'bW': '𝕎',
|
||||
\ 'bX': '𝕏',
|
||||
\ 'bY': '𝕐',
|
||||
\ 'bZ': 'ℤ',
|
||||
\ 'b0': '𝟘',
|
||||
\ 'b1': '𝟙',
|
||||
\ 'b2': '𝟚',
|
||||
\ 'b3': '𝟛',
|
||||
\ 'b4': '𝟜',
|
||||
\ 'b5': '𝟝',
|
||||
\ 'b6': '𝟞',
|
||||
\ 'b7': '𝟟',
|
||||
\ 'b8': '𝟠',
|
||||
\ 'b9': '𝟡',
|
||||
\ 'bsum': '⅀',
|
||||
\})
|
||||
|
||||
" Math chars
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'McA': '𝓐',
|
||||
\ 'McB': '𝓑',
|
||||
\ 'McC': '𝓒',
|
||||
\ 'McD': '𝓓',
|
||||
\ 'McE': '𝓔',
|
||||
\ 'McF': '𝓕',
|
||||
\ 'McG': '𝓖',
|
||||
\ 'McH': '𝓗',
|
||||
\ 'McI': '𝓘',
|
||||
\ 'McJ': '𝓙',
|
||||
\ 'McK': '𝓚',
|
||||
\ 'McL': '𝓛',
|
||||
\ 'McM': '𝓜',
|
||||
\ 'McN': '𝓝',
|
||||
\ 'McO': '𝓞',
|
||||
\ 'McP': '𝓟',
|
||||
\ 'McQ': '𝓠',
|
||||
\ 'McR': '𝓡',
|
||||
\ 'McS': '𝓢',
|
||||
\ 'McT': '𝓣',
|
||||
\ 'McU': '𝓤',
|
||||
\ 'McV': '𝓥',
|
||||
\ 'McW': '𝓦',
|
||||
\ 'McX': '𝓧',
|
||||
\ 'McY': '𝓨',
|
||||
\ 'McZ': '𝓩',
|
||||
\ 'Mca': '𝒶',
|
||||
\ 'Mcb': '𝒷',
|
||||
\ 'Mcc': '𝒸',
|
||||
\ 'Mcd': '𝒹',
|
||||
\ 'Mcf': '𝒻',
|
||||
\ 'Mch': '𝒽',
|
||||
\ 'Mci': '𝒾',
|
||||
\ 'Mcj': '𝒿',
|
||||
\ 'Mck': '𝓀',
|
||||
\ 'Mcl': '𝓁',
|
||||
\ 'Mcm': '𝓂',
|
||||
\ 'Mcn': '𝓃',
|
||||
\ 'Mcp': '𝓅',
|
||||
\ 'Mcq': '𝓆',
|
||||
\ 'Mcr': '𝓇',
|
||||
\ 'Mcs': '𝓈',
|
||||
\ 'Mct': '𝓉',
|
||||
\ 'Mcu': '𝓊',
|
||||
\ 'Mcv': '𝓋',
|
||||
\ 'Mcw': '𝓌',
|
||||
\ 'Mcx': '𝓍',
|
||||
\ 'Mcy': '𝓎',
|
||||
\ 'Mcz': '𝓏',
|
||||
\ 'MfA': '𝔄',
|
||||
\ 'MfB': '𝔅',
|
||||
\ 'MfD': '𝔇',
|
||||
\ 'MfE': '𝔈',
|
||||
\ 'MfF': '𝔉',
|
||||
\ 'MfG': '𝔊',
|
||||
\ 'MfJ': '𝔍',
|
||||
\ 'MfK': '𝔎',
|
||||
\ 'MfL': '𝔏',
|
||||
\ 'MfM': '𝔐',
|
||||
\ 'MfN': '𝔑',
|
||||
\ 'MfO': '𝔒',
|
||||
\ 'MfP': '𝔓',
|
||||
\ 'MfQ': '𝔔',
|
||||
\ 'MfS': '𝔖',
|
||||
\ 'MfT': '𝔗',
|
||||
\ 'MfU': '𝔘',
|
||||
\ 'MfV': '𝔙',
|
||||
\ 'MfW': '𝔚',
|
||||
\ 'MfX': '𝔛',
|
||||
\ 'MfY': '𝔜',
|
||||
\ 'Mfa': '𝔞',
|
||||
\ 'Mfb': '𝔟',
|
||||
\ 'Mfc': '𝔠',
|
||||
\ 'Mfd': '𝔡',
|
||||
\ 'Mfe': '𝔢',
|
||||
\ 'Mff': '𝔣',
|
||||
\ 'Mfg': '𝔤',
|
||||
\ 'Mfh': '𝔥',
|
||||
\ 'Mfi': '𝔦',
|
||||
\ 'Mfj': '𝔧',
|
||||
\ 'Mfk': '𝔨',
|
||||
\ 'Mfl': '𝔩',
|
||||
\ 'Mfm': '𝔪',
|
||||
\ 'Mfn': '𝔫',
|
||||
\ 'Mfo': '𝔬',
|
||||
\ 'Mfp': '𝔭',
|
||||
\ 'Mfq': '𝔮',
|
||||
\ 'Mfr': '𝔯',
|
||||
\ 'Mfs': '𝔰',
|
||||
\ 'Mft': '𝔱',
|
||||
\ 'Mfu': '𝔲',
|
||||
\ 'Mfv': '𝔳',
|
||||
\ 'Mfw': '𝔴',
|
||||
\ 'Mfx': '𝔵',
|
||||
\ 'Mfy': '𝔶',
|
||||
\ 'Mfz': '𝔷',
|
||||
\})
|
||||
|
||||
" From Favonia
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'breve': '˘',
|
||||
\ 'monus': '∸',
|
||||
\ '<>': '⟨⟩<left>',
|
||||
\ 'greekq': ';',
|
||||
\})
|
||||
|
||||
lockvar g:agda#default_glyphs
|
||||
endif
|
||||
|
||||
if !exists('g:agda#glyphs')
|
||||
let g:agda#glyphs = deepcopy(g:agda#default_glyphs)
|
||||
endif
|
||||
|
||||
let &cpo = s:cpo_save
|
88
nix/nvim-agda/agda-vim-excerpts/ftplugin.vim
Normal file
88
nix/nvim-agda/agda-vim-excerpts/ftplugin.vim
Normal file
|
@ -0,0 +1,88 @@
|
|||
let s:cpo_save = &cpo
|
||||
set cpo&vim
|
||||
|
||||
let b:undo_ftplugin = ''
|
||||
|
||||
for [sequence, symbol] in items(g:agda#glyphs)
|
||||
execute printf('noremap! <buffer> <LocalLeader>%s %s', sequence, symbol)
|
||||
endfor
|
||||
|
||||
setlocal matchpairs&vim
|
||||
setlocal matchpairs+=(:)
|
||||
setlocal matchpairs+=<:>
|
||||
setlocal matchpairs+=[:]
|
||||
setlocal matchpairs+={:}
|
||||
setlocal matchpairs+=«:»
|
||||
setlocal matchpairs+=‹:›
|
||||
setlocal matchpairs+=⁅:⁆
|
||||
setlocal matchpairs+=⁽:⁾
|
||||
setlocal matchpairs+=₍:₎
|
||||
setlocal matchpairs+=⌈:⌉
|
||||
setlocal matchpairs+=⌊:⌋
|
||||
setlocal matchpairs+=〈:〉
|
||||
setlocal matchpairs+=⎛:⎞
|
||||
setlocal matchpairs+=⎝:⎠
|
||||
setlocal matchpairs+=⎡:⎤
|
||||
setlocal matchpairs+=⎣:⎦
|
||||
setlocal matchpairs+=⎧:⎫
|
||||
setlocal matchpairs+=⎨:⎬
|
||||
setlocal matchpairs+=⎩:⎭
|
||||
setlocal matchpairs+=⎴:⎵
|
||||
setlocal matchpairs+=❨:❩
|
||||
setlocal matchpairs+=❪:❫
|
||||
setlocal matchpairs+=❬:❭
|
||||
setlocal matchpairs+=❮:❯
|
||||
setlocal matchpairs+=❰:❱
|
||||
setlocal matchpairs+=❲:❳
|
||||
setlocal matchpairs+=❴:❵
|
||||
setlocal matchpairs+=⟅:⟆
|
||||
setlocal matchpairs+=⟦:⟧
|
||||
setlocal matchpairs+=⟨:⟩
|
||||
setlocal matchpairs+=⟪:⟫
|
||||
setlocal matchpairs+=⦃:⦄
|
||||
setlocal matchpairs+=⦅:⦆
|
||||
setlocal matchpairs+=⦇:⦈
|
||||
setlocal matchpairs+=⦉:⦊
|
||||
setlocal matchpairs+=⦋:⦌
|
||||
setlocal matchpairs+=⦍:⦎
|
||||
setlocal matchpairs+=⦏:⦐
|
||||
setlocal matchpairs+=⦑:⦒
|
||||
setlocal matchpairs+=⦓:⦔
|
||||
setlocal matchpairs+=⦕:⦖
|
||||
setlocal matchpairs+=⦗:⦘
|
||||
setlocal matchpairs+=⸠:⸡
|
||||
setlocal matchpairs+=⸢:⸣
|
||||
setlocal matchpairs+=⸤:⸥
|
||||
setlocal matchpairs+=⸦:⸧
|
||||
setlocal matchpairs+=⸨:⸩
|
||||
setlocal matchpairs+=〈:〉
|
||||
setlocal matchpairs+=《:》
|
||||
setlocal matchpairs+=「:」
|
||||
setlocal matchpairs+=『:』
|
||||
setlocal matchpairs+=【:】
|
||||
setlocal matchpairs+=〔:〕
|
||||
setlocal matchpairs+=〖:〗
|
||||
setlocal matchpairs+=〘:〙
|
||||
setlocal matchpairs+=〚:〛
|
||||
setlocal matchpairs+=︗:︘
|
||||
setlocal matchpairs+=︵:︶
|
||||
setlocal matchpairs+=︷:︸
|
||||
setlocal matchpairs+=︹:︺
|
||||
setlocal matchpairs+=︻:︼
|
||||
setlocal matchpairs+=︽:︾
|
||||
setlocal matchpairs+=︿:﹀
|
||||
setlocal matchpairs+=﹁:﹂
|
||||
setlocal matchpairs+=﹃:﹄
|
||||
setlocal matchpairs+=﹇:﹈
|
||||
setlocal matchpairs+=﹙:﹚
|
||||
setlocal matchpairs+=﹛:﹜
|
||||
setlocal matchpairs+=﹝:﹞
|
||||
setlocal matchpairs+=(:)
|
||||
setlocal matchpairs+=<:>
|
||||
setlocal matchpairs+=[:]
|
||||
setlocal matchpairs+={:}
|
||||
setlocal matchpairs+=⦅:⦆
|
||||
setlocal matchpairs+=「:」
|
||||
let b:undo_ftplugin .= ' | setlocal matchpairs<'
|
||||
|
||||
let &cpo = s:cpo_save
|
26
nix/nvim-agda/default.nix
Normal file
26
nix/nvim-agda/default.nix
Normal file
|
@ -0,0 +1,26 @@
|
|||
{ nixpkgs, system, ... }:
|
||||
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
in
|
||||
pkgs.vimUtils.buildVimPlugin rec {
|
||||
pname = "nvim-agda";
|
||||
version = "2bed0b9a1d42f20438d22a3229c59faaf2b6a8df";
|
||||
src = pkgs.fetchFromGitHub {
|
||||
owner = "ashinkarov";
|
||||
repo = pname;
|
||||
rev = version;
|
||||
hash = "sha256-cMEOSGMyFHp/iABjpbxb3GFi4lBFYOhIDcI/EwgVgdw=";
|
||||
};
|
||||
buildPhase = ''
|
||||
for patch in ${./patches}/*; do
|
||||
echo Applying $patch...
|
||||
patch -p1 --verbose < $patch
|
||||
done
|
||||
|
||||
mkdir autoload
|
||||
cp ${agda-vim-excerpts/autoload.vim} autoload/agda.vim
|
||||
cat ${agda-vim-excerpts/ftplugin.vim} >> ftplugin/agda.vim
|
||||
cat ${./keybinds.vim} >> ftplugin/agda.vim
|
||||
'';
|
||||
}
|
11
nix/nvim-agda/keybinds.vim
Normal file
11
nix/nvim-agda/keybinds.vim
Normal file
|
@ -0,0 +1,11 @@
|
|||
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>
|
||||
nmap <buffer> K :<c-u>AgdaTypeContext<cr>
|
||||
nnoremap <buffer> [g :<c-u>GoalPrev<cr>
|
||||
nnoremap <buffer> ]g :<c-u>GoalNext<cr>
|
||||
nnoremap <buffer> gd :<c-u>AgdaWhyInscope<cr>
|
31
nix/nvim-agda/patches/0001-remove-default-keybinds.patch
Normal file
31
nix/nvim-agda/patches/0001-remove-default-keybinds.patch
Normal file
|
@ -0,0 +1,31 @@
|
|||
diff --git a/ftplugin/agda.vim b/ftplugin/agda.vim
|
||||
index f3264b5..2585b54 100644
|
||||
--- a/ftplugin/agda.vim
|
||||
+++ b/ftplugin/agda.vim
|
||||
@@ -39,26 +39,3 @@ command! GoalPrev :call AgdaMod.agda_goal_prev(expand("%:p"))
|
||||
command! AgdaCloseMsg :call AgdaMod.close_msg_win()
|
||||
command! GoalContent :call AgdaMod.gc()
|
||||
command! GetEvbuf :call AgdaMod.getevbuf()
|
||||
-
|
||||
-
|
||||
-" Key mappings
|
||||
-nm <buffer> <LocalLeader>l :<c-u>AgdaLoad<cr>
|
||||
-nm <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
|
||||
-nm <buffer> <LocalLeader>, :<c-u>AgdaTypeContext<cr>
|
||||
-nm <buffer> <LocalLeader>u, :<c-u>AgdaTypeContextNorm<cr>
|
||||
-nm <buffer> <LocalLeader>d :<c-u>AgdaInfer<cr>
|
||||
-nm <buffer> <LocalLeader>r :<c-u>AgdaRefine<cr>
|
||||
-nm <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
|
||||
-nm <buffer> <LocalLeader>n :<c-u>AgdaCompute<cr>
|
||||
-nm <buffer> <LocalLeader>a :<c-u>AgdaAuto<cr>
|
||||
-nm <buffer> <LocalLeader>h :<c-u>AgdaHelperFun<cr>
|
||||
-nm <buffer> <LocalLeader>o :<c-u>AgdaModuleContents<cr>
|
||||
-nm <buffer> <LocalLeader>w :<c-u>AgdaWhyInscope<cr>
|
||||
-nm <buffer> <LocalLeader>e :<c-u>MkPrompt<cr>
|
||||
-nm <buffer> <LocalLeader>? :<c-u>PrintGoals<cr>
|
||||
-nm <buffer> <LocalLeader>f :<c-u>GoalNext<cr>
|
||||
-nm <buffer> <LocalLeader>b :<c-u>GoalPrev<cr>
|
||||
-
|
||||
-
|
||||
-" mappings
|
||||
-runtime agda-input.vim
|
1
questions.txt
Normal file
1
questions.txt
Normal file
|
@ -0,0 +1 @@
|
|||
_<_ why is one constructor allowed to only have one
|
34
src/Extra2.agda
Normal file
34
src/Extra2.agda
Normal file
|
@ -0,0 +1,34 @@
|
|||
module _ where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
|
||||
record ⊤ : Set where
|
||||
constructor tt
|
||||
|
||||
postulate
|
||||
tt′ : ⊤
|
||||
|
||||
lemma₀ : tt ≡ tt′
|
||||
lemma₀ = refl
|
||||
|
||||
open import Data.Nat
|
||||
open import Data.Nat.Properties
|
||||
|
||||
record Terminating (n : ℕ) : Set where
|
||||
inductive
|
||||
constructor box
|
||||
field
|
||||
call : ∀ {m : ℕ} → m <′ n → Terminating m
|
||||
open Terminating
|
||||
|
||||
term : ∀ (n : ℕ) → Terminating n
|
||||
term 0 .call ()
|
||||
term (suc n) .call ≤′-refl = term n
|
||||
term (suc n) .call (≤′-step sm≤n) = term n .call sm≤n
|
||||
|
||||
postulate
|
||||
_/2 : ℕ → ℕ
|
||||
/2-<′ : ∀ (n : ℕ) → n /2 <′ n
|
||||
|
||||
merge : (n : ℕ) → Terminating n → ℕ
|
||||
merge n (box caller) = merge (n /2) (caller (/2-<′ n))
|
87
src/Extra3.agda
Normal file
87
src/Extra3.agda
Normal file
|
@ -0,0 +1,87 @@
|
|||
module _ where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning
|
||||
open import Function
|
||||
open import Data.Nat
|
||||
open import Data.Fin hiding (_+_)
|
||||
open import Data.Product hiding (map)
|
||||
|
||||
-- Functions as Lists
|
||||
|
||||
Vec : Set → ℕ → Set
|
||||
Vec A n = Fin n → A
|
||||
|
||||
map-Vec : {A B : Set} {n : ℕ} → (A → B) → Vec A n → Vec B n
|
||||
map-Vec f v = f ∘′ v
|
||||
|
||||
map-Vec-compose : {A B C : Set} {n : ℕ} (f : B → C) (g : A → B) (v : Vec A n)
|
||||
→ map-Vec (f ∘ g) v ≡ map-Vec f (map-Vec g v)
|
||||
map-Vec-compose f g v = refl
|
||||
|
||||
List : Set → Set
|
||||
List A = Σ ℕ (λ n → Vec A n)
|
||||
|
||||
map : {A B : Set} → (A → B) → List A → List B
|
||||
map f (n , v) = n , (f ∘′ v)
|
||||
|
||||
map-compose : {A B C : Set} (f : B → C) (g : A → B) (l : List A)
|
||||
→ map (f ∘ g) l ≡ map f (map g l)
|
||||
map-compose f g l = refl
|
||||
|
||||
[] : {A : Set} → List A
|
||||
[] = 0 , λ ()
|
||||
|
||||
_∷_ : {A : Set} → A → List A → List A
|
||||
a ∷ (n , v) = (suc n) , λ{ zero → a ; (suc n) → v n }
|
||||
|
||||
--- Questions
|
||||
|
||||
-- Q1: Instance arguments...
|
||||
-- A1: Don't abuse it
|
||||
|
||||
-- Q2: Convervativity of the eta rule of sigma types
|
||||
-- A2: this is a very interesting question!!!
|
||||
--
|
||||
-- ETT is conservative with respect to (ITT + K) + function ext, by Martin Hofmann
|
||||
|
||||
-- Q3: Differences between judgmental eq, propositional eq, and isomorphisms
|
||||
|
||||
-- A3: Judgmental equality is given
|
||||
|
||||
_ = 1 + 1 ≡ 2
|
||||
_ = refl
|
||||
|
||||
-- Propositional equality is a type that can be either
|
||||
|
||||
-- 1. the inductive types generated by reflexivity, or
|
||||
-- 2. ...
|
||||
-- 3. ...
|
||||
|
||||
-- Isomorphisms only make sense between two types.
|
||||
|
||||
-- Q4: syntax
|
||||
|
||||
postulate
|
||||
F : (Set → Set) → (Set → Set)
|
||||
|
||||
syntax F (λ x → e) (λ y → f) = e - x - y - f
|
||||
|
||||
-- Q5. subtying in kinds
|
||||
|
||||
-- Speed coding
|
||||
|
||||
+-comm : ∀ n m → n + m ≡ m + n
|
||||
+-comm 0 m = ?
|
||||
+-comm (suc n) m =
|
||||
begin
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
m + suc n
|
||||
∎
|
221
src/Homework1.agda
Normal file
221
src/Homework1.agda
Normal file
|
@ -0,0 +1,221 @@
|
|||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
|
||||
open ≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_)
|
||||
open import Data.Nat.Properties using (+-identityʳ; +-assoc; +-suc; +-comm)
|
||||
|
||||
module Homework1 where
|
||||
|
||||
-- zero property
|
||||
0-prop : ∀ (n : ℕ) → n * 0 ≡ 0
|
||||
0-prop zero = refl
|
||||
0-prop (suc n) = 0-prop n
|
||||
|
||||
-- multiplicative identity
|
||||
*-identity : ∀ (n : ℕ) → n * 1 ≡ n
|
||||
*-identity zero = refl
|
||||
*-identity (suc n) =
|
||||
begin
|
||||
suc n * 1
|
||||
≡⟨⟩
|
||||
1 + n * 1
|
||||
≡⟨ cong (1 +_) (*-identity n) ⟩
|
||||
1 + n
|
||||
∎
|
||||
|
||||
|
||||
-- multiplicative commutativity
|
||||
-- using induction on both variables
|
||||
*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
|
||||
*-comm zero zero = refl
|
||||
*-comm a zero = 0-prop a
|
||||
*-comm zero b = sym (0-prop b)
|
||||
*-comm (suc a) (suc b) =
|
||||
begin
|
||||
suc a * suc b
|
||||
≡⟨⟩
|
||||
suc b + a * suc b
|
||||
≡⟨ cong (suc b +_) (*-comm a (suc b)) ⟩
|
||||
suc b + suc b * a
|
||||
≡⟨⟩
|
||||
suc b + (a + b * a)
|
||||
≡⟨ sym (+-assoc (suc b) a (b * a)) ⟩
|
||||
suc b + a + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-comm (suc b) a) ⟩
|
||||
a + suc b + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-suc a b) ⟩
|
||||
suc (a + b) + b * a
|
||||
≡⟨ cong (_+ (b * a)) (cong suc (+-comm a b)) ⟩
|
||||
suc (b + a) + b * a
|
||||
≡⟨ cong (_+ (b * a)) (sym (+-suc b a)) ⟩
|
||||
b + suc a + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-comm b (suc a)) ⟩
|
||||
suc a + b + b * a
|
||||
≡⟨ cong (suc a + b +_) (*-comm b a) ⟩
|
||||
suc a + b + a * b
|
||||
≡⟨ +-assoc (suc a) b (a * b) ⟩
|
||||
suc a + (b + a * b)
|
||||
≡⟨⟩
|
||||
suc a + suc a * b
|
||||
≡⟨ cong (suc a +_) (*-comm (suc a) b) ⟩
|
||||
suc a + b * suc a
|
||||
≡⟨⟩
|
||||
suc b * suc a
|
||||
∎
|
||||
|
||||
-- multiplication distributive property
|
||||
*-distrib-+ : ∀ (a b c : ℕ) → a * (b + c) ≡ (a * b) + (a * c)
|
||||
*-distrib-+ a zero c =
|
||||
begin
|
||||
a * (zero + c)
|
||||
≡⟨⟩
|
||||
a * c
|
||||
≡⟨⟩
|
||||
zero + (a * c)
|
||||
≡⟨ cong (_+ (a * c)) (sym (0-prop a)) ⟩
|
||||
(a * zero) + (a * c)
|
||||
∎
|
||||
*-distrib-+ a (suc b) c =
|
||||
begin
|
||||
a * (suc b + c)
|
||||
≡⟨⟩
|
||||
a * suc (b + c)
|
||||
≡⟨ *-comm a (suc (b + c)) ⟩
|
||||
suc (b + c) * a
|
||||
≡⟨⟩
|
||||
a + (b + c) * a
|
||||
≡⟨ cong (a +_) (*-comm (b + c) a) ⟩
|
||||
a + a * (b + c)
|
||||
≡⟨ cong (a +_) (*-distrib-+ a b c) ⟩
|
||||
a + ((a * b) + (a * c))
|
||||
≡⟨ cong (a +_) (cong (_+ (a * c)) (*-comm a b)) ⟩
|
||||
a + ((b * a) + (a * c))
|
||||
≡⟨ sym (+-assoc a (b * a) (a * c)) ⟩
|
||||
a + (b * a) + (a * c)
|
||||
≡⟨⟩
|
||||
(suc b * a) + (a * c)
|
||||
≡⟨ cong (_+ (a * c)) (*-comm (suc b) a) ⟩
|
||||
(a * suc b) + (a * c)
|
||||
∎
|
||||
|
||||
|
||||
-- multiplicative associativity
|
||||
*-assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
|
||||
*-assoc zero b c = refl
|
||||
*-assoc (suc a) b c =
|
||||
begin
|
||||
(suc a * b) * c
|
||||
≡⟨⟩
|
||||
(b + a * b) * c
|
||||
≡⟨ *-comm (b + a * b) c ⟩
|
||||
c * (b + a * b)
|
||||
≡⟨ *-distrib-+ c b (a * b) ⟩
|
||||
(c * b) + (c * (a * b))
|
||||
≡⟨ cong ((c * b) +_) (sym (*-assoc c a b)) ⟩
|
||||
(c * b) + (c * a * b)
|
||||
≡⟨ cong (_+ (c * a * b)) (*-comm c b) ⟩
|
||||
(b * c) + (c * a * b)
|
||||
≡⟨ cong ((b * c) +_) (cong (_* b) (*-comm c a)) ⟩
|
||||
(b * c) + (a * c * b)
|
||||
≡⟨ cong ((b * c) +_) (*-assoc a c b) ⟩
|
||||
(b * c) + (a * (c * b))
|
||||
≡⟨ cong ((b * c) +_) (cong (a *_) (*-comm c b)) ⟩
|
||||
(b * c) + (a * (b * c))
|
||||
∎
|
||||
|
||||
|
||||
-- 1-identity
|
||||
1-identity : ∀ (n : ℕ) → 1 * n ≡ n
|
||||
1-identity n =
|
||||
begin
|
||||
1 * n
|
||||
≡⟨⟩
|
||||
n + 0 * n
|
||||
≡⟨⟩
|
||||
n + 0
|
||||
≡⟨ +-comm n 0 ⟩
|
||||
0 + n
|
||||
≡⟨⟩
|
||||
n
|
||||
∎
|
||||
|
||||
-- exponentiation distributive property
|
||||
^-distribˡ-|-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
|
||||
^-distribˡ-|-* m zero p =
|
||||
begin
|
||||
m ^ (zero + p)
|
||||
≡⟨⟩
|
||||
m ^ p
|
||||
≡⟨ sym (1-identity (m ^ p)) ⟩
|
||||
1 * (m ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ zero) * (m ^ p)
|
||||
∎
|
||||
^-distribˡ-|-* m (suc n) p =
|
||||
begin
|
||||
m ^ (suc n + p)
|
||||
≡⟨⟩
|
||||
m ^ (suc (n + p))
|
||||
≡⟨⟩
|
||||
m * (m ^ (n + p))
|
||||
≡⟨ cong (m *_) (^-distribˡ-|-* m n p) ⟩
|
||||
m * ((m ^ n) * (m ^ p))
|
||||
≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
|
||||
(m * (m ^ n)) * (m ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ suc n) * (m ^ p)
|
||||
∎
|
||||
|
||||
-- exponential distribution from the right
|
||||
^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
|
||||
^-distribʳ-* m n zero = refl
|
||||
^-distribʳ-* m n (suc p) =
|
||||
begin
|
||||
(m * n) ^ (suc p)
|
||||
≡⟨⟩
|
||||
(m * n) * (m * n) ^ p
|
||||
≡⟨ cong (m * n *_) (^-distribʳ-* m n p) ⟩
|
||||
(m * n) * ((m ^ p) * (n ^ p))
|
||||
≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
|
||||
(m * n) * (m ^ p) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (*-assoc m n (m ^ p)) ⟩
|
||||
(m * (n * (m ^ p))) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (cong (m *_) (*-comm n (m ^ p))) ⟩
|
||||
(m * ((m ^ p) * n)) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (sym (*-assoc m (m ^ p) n)) ⟩
|
||||
m * (m ^ p) * n * (n ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ suc p) * n * (n ^ p)
|
||||
≡⟨ *-assoc (m ^ suc p) n (n ^ p) ⟩
|
||||
(m ^ suc p) * (n * (n ^ p))
|
||||
≡⟨⟩
|
||||
(m ^ suc p) * (n ^ suc p)
|
||||
∎
|
||||
|
||||
-- exponential association
|
||||
^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
|
||||
^-*-assoc m n zero =
|
||||
begin
|
||||
(m ^ n) ^ zero
|
||||
≡⟨⟩
|
||||
1
|
||||
≡⟨⟩
|
||||
m ^ zero
|
||||
≡⟨ cong (m ^_) (sym (0-prop n)) ⟩
|
||||
m ^ (n * zero)
|
||||
∎
|
||||
^-*-assoc m n (suc p) =
|
||||
begin
|
||||
(m ^ n) ^ (suc p)
|
||||
≡⟨⟩
|
||||
(m ^ n) * (m ^ n) ^ p
|
||||
≡⟨ cong (m ^ n *_) (^-*-assoc m n p) ⟩
|
||||
(m ^ n) * m ^ (n * p)
|
||||
≡⟨ sym (^-distribˡ-|-* m n (n * p)) ⟩
|
||||
m ^ (n + n * p)
|
||||
≡⟨ cong (m ^_) (cong (n +_) (*-comm n p)) ⟩
|
||||
m ^ (n + p * n)
|
||||
≡⟨⟩
|
||||
m ^ (suc p * n)
|
||||
≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
|
||||
m ^ (n * suc p)
|
||||
∎
|
77
src/Homework2.agda
Normal file
77
src/Homework2.agda
Normal file
|
@ -0,0 +1,77 @@
|
|||
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
|
||||
|
||||
-------------------------------------------------------
|
||||
-- from
|
||||
-------------------------------------------------------
|
||||
|
||||
from : Bin → ℕ
|
||||
from O = 0
|
||||
from (b I) = 1 + (from b) * 2
|
||||
from (b II) = 2 + (from b) * 2
|
||||
|
||||
-------------------------------------------------------
|
||||
-- to
|
||||
-------------------------------------------------------
|
||||
|
||||
inc : Bin → Bin
|
||||
inc O = O I
|
||||
inc (b I) = b II
|
||||
inc (b II) = (inc b) I
|
||||
|
||||
to : ℕ → Bin
|
||||
to 0 = O
|
||||
to (suc n) = inc (to n)
|
||||
|
||||
-------------------------------------------------------
|
||||
-- from∘to
|
||||
-------------------------------------------------------
|
||||
|
||||
from-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
|
||||
from-inc O = refl
|
||||
from-inc (n I) = refl
|
||||
from-inc (n II) = cong suc (cong (_* 2) (from-inc n))
|
||||
|
||||
from∘to : ∀ n → from (to n) ≡ n
|
||||
from∘to zero = refl
|
||||
from∘to (suc n) = trans (from-inc (to n)) (cong suc (from∘to n))
|
||||
|
||||
-------------------------------------------------------
|
||||
-- to∘from
|
||||
-------------------------------------------------------
|
||||
|
||||
toI : ∀ (n : ℕ) → to (1 + n * 2) ≡ (to n) I
|
||||
toI zero = refl
|
||||
toI (suc n) = cong inc (cong inc (toI n))
|
||||
|
||||
to∘from : ∀ b → to (from b) ≡ b
|
||||
to∘from O = refl
|
||||
to∘from (n I) =
|
||||
begin
|
||||
to (1 + (from n) * 2)
|
||||
≡⟨ toI (from n) ⟩
|
||||
(to (from n)) I
|
||||
≡⟨ cong _I (to∘from n) ⟩
|
||||
n I
|
||||
∎
|
||||
to∘from (n II) =
|
||||
begin
|
||||
to (from (n II))
|
||||
≡⟨⟩
|
||||
to (2 + (from n) * 2)
|
||||
≡⟨⟩
|
||||
inc (to (1 + (from n) * 2))
|
||||
≡⟨ cong inc (toI (from n)) ⟩
|
||||
inc ((to (from n)) I)
|
||||
≡⟨ cong inc (cong _I (to∘from n)) ⟩
|
||||
n II
|
||||
∎
|
77
src/Homework3.agda
Normal file
77
src/Homework3.agda
Normal file
|
@ -0,0 +1,77 @@
|
|||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
open import Homework3Prelude
|
||||
|
||||
module Homework3 where
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 1
|
||||
---------------------------------------------------------
|
||||
|
||||
V¬—→ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ ⊢ A}
|
||||
→ Value M
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 2
|
||||
---------------------------------------------------------
|
||||
|
||||
mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
mul = μ -- *
|
||||
ƛ -- m
|
||||
ƛ -- n
|
||||
(case (# 1) -- match on m
|
||||
-- case `zero → return 0
|
||||
(`zero)
|
||||
|
||||
-- case `suc m₁ → return n + (m₁ * n)
|
||||
(plus · # 1 · (# 3 · # 0 · # 1))
|
||||
)
|
||||
|
||||
task2 : mul {∅} · one · one —↠ one
|
||||
task2 =
|
||||
begin
|
||||
mul · one · one
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · one · one
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one `zero (plus · # 1 · (mul · # 0 · # 1)))) · one
|
||||
—→⟨ β-ƛ (V-suc V-zero) ⟩
|
||||
case one `zero (plus · one · (mul · # 0 · one))
|
||||
—→⟨ β-suc V-zero ⟩
|
||||
plus · one · (mul · `zero · one)
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · one · (mul · `zero · one)
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · (mul · `zero · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
((ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · `zero · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
((ƛ (case `zero `zero (plus · # 1 · (mul · # 0 · # 1)))) · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
(case `zero `zero (plus · one · (mul · # 0 · one)))
|
||||
—→⟨ ξ-·₂ V-ƛ β-zero ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · `zero
|
||||
—→⟨ β-ƛ V-zero ⟩
|
||||
case one `zero (`suc (plus · # 0 · `zero))
|
||||
—→⟨ β-suc V-zero ⟩
|
||||
`suc (plus · `zero · `zero)
|
||||
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
`suc ((ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · `zero · `zero)
|
||||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩
|
||||
`suc ((ƛ (case `zero (# 0) (`suc (plus · # 0 · # 1)))) · `zero)
|
||||
—→⟨ ξ-suc (β-ƛ V-zero) ⟩
|
||||
`suc (case `zero `zero (`suc (plus · # 0 · `zero)))
|
||||
—→⟨ ξ-suc β-zero ⟩
|
||||
one
|
||||
∎
|
241
src/Homework3Prelude.agda
Normal file
241
src/Homework3Prelude.agda
Normal file
|
@ -0,0 +1,241 @@
|
|||
-- This file contains the code extracted from the DeBruijn chapter in PLFA
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
|
||||
module Homework3Prelude where
|
||||
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_ : Context → Type → Context
|
||||
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A}
|
||||
---------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ A
|
||||
---------
|
||||
→ Γ , B ∋ A
|
||||
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
`_ : ∀ {Γ A}
|
||||
→ Γ ∋ A
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
ƛ_ : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A ⇒ B
|
||||
→ Γ ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
---------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc_ : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
----------
|
||||
→ Γ ⊢ A
|
||||
|
||||
μ_ : ∀ {Γ A}
|
||||
→ Γ , A ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
|
||||
length : Context → ℕ
|
||||
length ∅ = zero
|
||||
length (Γ , _) = suc (length Γ)
|
||||
|
||||
lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
|
||||
lookup {(_ , A)} {zero} (s≤s z≤n) = A
|
||||
lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p
|
||||
|
||||
count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
|
||||
count {_ , _} {zero} (s≤s z≤n) = Z
|
||||
count {Γ , _} {(suc n)} (s≤s p) = S (count p)
|
||||
|
||||
#_ : ∀ {Γ}
|
||||
→ (n : ℕ)
|
||||
→ {n∈Γ : True (suc n ≤? length Γ)}
|
||||
--------------------------------
|
||||
→ Γ ⊢ lookup (toWitness n∈Γ)
|
||||
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
|
||||
|
||||
one : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
one = `suc `zero
|
||||
|
||||
two : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
two = `suc `suc `zero
|
||||
|
||||
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
|
||||
|
||||
ext : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
|
||||
ext ρ Z = Z
|
||||
ext ρ (S x) = S (ρ x)
|
||||
|
||||
rename : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
|
||||
exts : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
|
||||
exts σ Z = ` Z
|
||||
exts σ (S x) = rename S_ (σ x)
|
||||
|
||||
subst : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , B ⊢ A
|
||||
→ Γ ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
|
||||
where
|
||||
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
|
||||
σ Z = M
|
||||
σ (S x) = ` x
|
||||
|
||||
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||
|
||||
V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
|
||||
---------------------------
|
||||
→ Value (ƛ N)
|
||||
|
||||
V-zero : ∀ {Γ}
|
||||
-----------------
|
||||
→ Value (`zero {Γ})
|
||||
|
||||
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
|
||||
→ L —→ L′
|
||||
---------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
|
||||
→ Value V
|
||||
→ M —→ M′
|
||||
---------------
|
||||
→ V · M —→ V · M′
|
||||
|
||||
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
|
||||
→ Value W
|
||||
--------------------
|
||||
→ (ƛ N) · W —→ N [ W ]
|
||||
|
||||
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
|
||||
→ M —→ M′
|
||||
-----------------
|
||||
→ `suc M —→ `suc M′
|
||||
|
||||
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ L —→ L′
|
||||
-------------------------
|
||||
→ case L M N —→ case L′ M N
|
||||
|
||||
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
-------------------
|
||||
→ case `zero M N —→ M
|
||||
|
||||
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ Value V
|
||||
----------------------------
|
||||
→ case (`suc V) M N —→ N [ V ]
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
----------------
|
||||
→ μ N —→ N [ μ N ]
|
||||
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_∎ : (M : Γ ⊢ A)
|
||||
------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
-- → L —↠ M
|
||||
→ M —↠ N
|
||||
------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
81
src/LambdaPi.agda
Normal file
81
src/LambdaPi.agda
Normal file
|
@ -0,0 +1,81 @@
|
|||
module LambdaPi where
|
||||
|
||||
open import Data.Nat using (ℕ; suc; _≟_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
open import Relation.Nullary using (yes; no; ¬_)
|
||||
|
||||
infix 4 _—→_
|
||||
infix 5 ƛ_
|
||||
infixl 7 _·_
|
||||
infix 9 `_
|
||||
infix 9 _[_:=_]
|
||||
|
||||
data Term : Set where
|
||||
-- var
|
||||
`_ : ℕ → Term
|
||||
|
||||
-- lam
|
||||
ƛ_ : Term → Term
|
||||
|
||||
-- app
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
data Value : Term → Set where
|
||||
-- lam is a value
|
||||
V-ƛ : ∀ {N} → Value (ƛ N)
|
||||
|
||||
----------------------------------------------------
|
||||
-- substitution
|
||||
----------------------------------------------------
|
||||
_[_:=_] : Term → ℕ → Term → Term
|
||||
|
||||
-- var
|
||||
(` n₁) [ n₂ := V ] with n₁ ≟ n₂
|
||||
... | yes _ = V
|
||||
... | no _ = ` n₁
|
||||
|
||||
-- lam
|
||||
(ƛ N) [ n := V ] = ƛ (N [ suc n := V ])
|
||||
|
||||
-- app
|
||||
(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
|
||||
|
||||
----------------------------------------------------
|
||||
-- reduction
|
||||
----------------------------------------------------
|
||||
data _—→_ : Term → Term → Set where
|
||||
-- beta reduction for lambda applications
|
||||
β-ƛ : ∀ {x N V} → Value V → (ƛ N) · V —→ N [ x := V ]
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing
|
||||
----------------------------------------------------
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing context
|
||||
----------------------------------------------------
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_::_ : Type → Context
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing judgment
|
||||
----------------------------------------------------
|
||||
data _⊢_⦂_ : Context → Term → Type → Set where
|
||||
|
||||
----------------------------------------------------
|
||||
-- progress
|
||||
----------------------------------------------------
|
||||
data Progress (M : Term) : Set where
|
||||
step : ∀ {N} → M —→ N → Progress M
|
||||
done : Value M → Progress M
|
||||
|
||||
progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
|
||||
|
||||
----------------------------------------------------
|
||||
-- preservation
|
||||
----------------------------------------------------
|
||||
preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
|
27
src/LambdaTest.agda
Normal file
27
src/LambdaTest.agda
Normal file
|
@ -0,0 +1,27 @@
|
|||
module LambdaTest where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
using (_≡_; _≢_; refl; sym; cong; cong₂)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Nat using (ℕ; zero; suc)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Product
|
||||
using (_×_; proj₁; proj₂; ∃; ∃-syntax)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Function using (_∘_)
|
||||
V¬—→ V-ƛ = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) (ξ-suc m) = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) = ?
|
||||
open import plfa.part2.Lambda
|
||||
|
||||
V¬—→ : ∀ {M N}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
30
src/OtherShit.agda
Normal file
30
src/OtherShit.agda
Normal file
|
@ -0,0 +1,30 @@
|
|||
module OtherShit where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning
|
||||
open import Data.Nat
|
||||
open import Data.Nat.Properties
|
||||
open import Data.Unit
|
||||
open import Data.Empty
|
||||
|
||||
data Bin : Set where
|
||||
O : Bin
|
||||
_I : Bin → Bin
|
||||
_II : Bin → Bin
|
||||
|
||||
data even : ℕ → Set
|
||||
data odd : ℕ → Set
|
||||
|
||||
data even where
|
||||
zero : even zero
|
||||
suc : ∀ {n : ℕ} → odd n → even (suc n)
|
||||
|
||||
data odd where
|
||||
suc : ∀ {n : ℕ} → even n → odd (suc n)
|
||||
|
||||
to : ℕ → Bin
|
||||
to zero = O
|
||||
to n with odd n
|
||||
... | x = O I
|
||||
to n with even n
|
||||
... | x = O II
|
19
src/Project/Lambda1.agda
Normal file
19
src/Project/Lambda1.agda
Normal file
|
@ -0,0 +1,19 @@
|
|||
module Project.Lambda1 where
|
||||
|
||||
open import Data.Nat using (ℕ; suc; _≟_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
open import Relation.Nullary using (yes; no; ¬_)
|
||||
|
||||
data Term : Set where
|
||||
`_ : ℕ → Term
|
||||
ƛ_ : Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
`suc _ : Term → Term
|
||||
`zero : Term
|
||||
|
||||
data Value : Term → Set where
|
||||
V-ƛ : ∀ {N} → Value (ƛ N)
|
||||
|
||||
data Context : Set where
|
||||
⊙ : Context
|
|
@ -868,7 +868,17 @@ just apply the previous results which show addition
|
|||
is associative and commutative.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
|
||||
+-swap m n p =
|
||||
begin
|
||||
m + (n + p)
|
||||
≡⟨ sym (+-assoc m n p) ⟩
|
||||
(m + n) + p
|
||||
≡⟨ cong (_+ p) (+-comm m n) ⟩
|
||||
(n + m) + p
|
||||
≡⟨ +-assoc n m p ⟩
|
||||
n + (m + p)
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
|
@ -881,7 +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
|
||||
≡⟨ 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
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
|
@ -895,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
|
||||
≡⟨ ⟩
|
||||
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
|
|
|
@ -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
|
||||
```
|
||||
|
||||
|
||||
|
|
|
@ -754,7 +754,15 @@ successor of the sum of two even numbers, which is even.
|
|||
Show that the sum of two odd numbers is even.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
import Data.Nat.Properties
|
||||
open Data.Nat.Properties using (+-suc)
|
||||
|
||||
o+o≡e : ∀ {m n : ℕ}
|
||||
→ odd m → odd n
|
||||
→ even (m + n)
|
||||
|
||||
-- o+o≡e om (suc en) = suc (+-suc (o+e≡o om en))
|
||||
o+o≡e om (suc en) = +-suc ?
|
||||
```
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}
|
||||
|
|
|
@ -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
|
||||
|
||||
```
|
||||
|
||||
|
||||
|
@ -1038,7 +1056,34 @@ to the list
|
|||
[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
open import plfa.part1.Isomorphism using (_≃_)
|
||||
open import Data.Product using (_×_; _,_)
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning renaming (begin_ to begin-≡_; _∎ to _∎-≡)
|
||||
|
||||
contextOfList : (l : List (Id × Type)) → Context
|
||||
contextOfList [] = ∅
|
||||
contextOfList ((id , type) ∷ l) = (contextOfList l) , id ⦂ type
|
||||
|
||||
listOfContext : (c : Context) → List (Id × Type)
|
||||
listOfContext ∅ = []
|
||||
listOfContext (c , x ⦂ x₁) = (x , x₁) ∷ listOfContext c
|
||||
|
||||
contextListIso : (c : Context) → contextOfList (listOfContext c) ≡ c
|
||||
contextListIso ∅ = refl
|
||||
contextListIso (c , x ⦂ x₁) = cong (_, x ⦂ x₁) (contextListIso c)
|
||||
|
||||
listContextIso : (l : List (Id × Type)) → listOfContext (contextOfList l) ≡ l
|
||||
listContextIso [] = refl
|
||||
listContextIso (x ∷ l) = cong (x ∷_) (listContextIso l)
|
||||
|
||||
Context≃List : Context ≃ List (Id × Type)
|
||||
Context≃List = record
|
||||
{ from = contextOfList
|
||||
; to = listOfContext
|
||||
; from∘to = contextListIso
|
||||
; to∘from = listContextIso
|
||||
}
|
||||
```
|
||||
|
||||
### Lookup judgment
|
||||
|
|
Loading…
Reference in a new issue