Switch to Hakyll as the build system for PLFA (#540)

This commit is contained in:
Wen Kokke 2020-10-23 08:45:49 +02:00 committed by GitHub
parent ea8bee4461
commit 2c82ce21da
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
509 changed files with 103793 additions and 1327 deletions

View file

@ -9,7 +9,3 @@ else
echo "Checking for whitespace violations..." echo "Checking for whitespace violations..."
fix-whitespace --check fix-whitespace --check
fi fi
# Run the test suite.
echo "Running the test suite..."
make test-offline

10
.gitignore vendored
View file

@ -3,6 +3,13 @@
.agda-stdlib.sed .agda-stdlib.sed
.links-*.sed .links-*.sed
## Haskell files
_site/
_cache/
stack.yaml.lock
.stack-work/
dist-newstyle
## Jekyll files ## Jekyll files
_site/ _site/
.sass-cache/ .sass-cache/
@ -26,4 +33,5 @@ auto/
## Misc build files ## Misc build files
out/ out/
.versions/ *.zip
versions/plfa.github.io-web-*/

3
.gitmodules vendored Normal file
View file

@ -0,0 +1,3 @@
[submodule "standard-library"]
path = standard-library
url = git@github.com:agda/agda-stdlib.git

24
404.html Executable file
View file

@ -0,0 +1,24 @@
---
layout: default
---
<style type="text/css" media="screen">
.container {
margin: 10px auto;
max-width: 600px;
text-align: center;
}
h1 {
margin: 30px 0;
font-size: 4em;
line-height: 1;
letter-spacing: -1px;
}
</style>
<div class="container">
<h1>404</h1>
<p><strong>Page not found :(</strong></p>
<p>The requested page could not be found.</p>
</div>

17
Gemfile
View file

@ -1,19 +1,8 @@
# NOTE: the Gemfile is no longer used by the main distribution of PLFA,
# but is still used to build legacy versions 19.07 and 20.08.
source "https://rubygems.org" source "https://rubygems.org"
group :jekyll_plugins do group :jekyll_plugins do
gem 'github-pages' gem 'github-pages'
end end
group :development do
gem 'guard'
gem 'guard-shell'
gem 'html-proofer'
# ffi-1.13.1 is broken on macos
# https://github.com/ffi/ffi/issues/791
gem 'ffi', '~> 1.12.2'
end
group :epub do
gem 'safe_yaml'
gem 'liquid'
end

View file

@ -1,9 +0,0 @@
require 'fileutils'
guard :shell do
watch(%r{^(.+)\.lagda\.md$}) do |m|
src = m[0]
out = "#{File.dirname(src).sub('src','out')}/#{File.basename(src,'.lagda.md')}.md"
`make #{out}` unless File.basename(src).start_with?('.#')
end
end

429
Makefile
View file

@ -1,273 +1,202 @@
SHELL := /usr/bin/env bash #################################################################################
AGDA_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.lagda.md') # Configuration
AGDAI_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.agdai') #################################################################################
MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
PANDOC := pandoc
EPUBCHECK := epubcheck
RUBY := ruby
GEM := $(RUBY) -S gem
BUNDLE := $(RUBY) -S bundle
JEKYLL := $(BUNDLE) exec jekyll
HTMLPROOFER := $(BUNDLE) exec htmlproofer
LUA_FILES := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
RELEASE_VERSIONS := 19.08 20.07
RELEASES := $(addsuffix /,$(RELEASE_VERSIONS))
LATEST_VERSION := $(word $(words $(RELEASE_VERSIONS)),$(RELEASE_VERSIONS))
ifeq ($(AGDA_STDLIB_VERSION),) SITE_DIR := _site
AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/ CACHE_DIR := _cache
else TMP_DIR := $(CACHE_DIR)/tmp
AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/v$(AGDA_STDLIB_VERSION)/
#################################################################################
# Setup Git Hooks
#################################################################################
.PHONY: init
init: setup-check-fix-whitespace setup-check-htmlproofer
git config core.hooksPath .githooks
#################################################################################
# Build PLFA site
#################################################################################
.PHONY: build
build: $(SITE_DIR)
$(SITE_DIR): authors contributors css courses hs posts public src templates
stack build && stack exec site build
#################################################################################
# Test generated site with HTMLProofer
#################################################################################
.PHONY: test
test: setup-install-htmlproofer $(SITE_DIR)
cd $(SITE_DIR) && htmlproofer \
--check-html \
--disable-external \
--report-invalid-tags \
--report-missing-names \
--report-script-embeds \
--report-missing-doctype \
--report-eof-tags \
--report-mismatched-tags \
--check-img-http \
--check-opengraph \
.
#################################################################################
# Test generated EPUB with EPUBCheck
#################################################################################
.PHONY: test-epub
test-epub: setup-check-epubcheck $(SITE_DIR)/plfa.epub
epubcheck $(SITE_DIR)/plfa.epub
#################################################################################
# Automatically rebuild the site on changes, and start a preview server
#################################################################################
.PHONY: watch
watch:
stack build && stack exec site watch
#################################################################################
# Update contributor metadata in `contributors/`
#################################################################################
.PHONY: update-contributors
update-contributors:
stack build && stack exec update-contributors
#################################################################################
# Clean up and remove the cache
#################################################################################
.PHONY: clean
clean:
stack build && stack exec site clean
#################################################################################
# List targets in Makefile
#################################################################################
.PHONY: list
list:
@$(MAKE) -pRrq -f $(lastword $(MAKEFILE_LIST)) : 2>/dev/null | awk -v RS= -F: '/^# File/,/^# Finished Make data base/ {if ($$1 !~ "^[#.]") {print $$1}}' | sort | egrep -v -e '^[^[:alnum:]]' -e '^$@$$'
#################################################################################
# Setup dependencies
#################################################################################
.PHONY: setup-check-stack
setup-check-stack:
ifeq (,$(wildcard $(shell which stack)))
@echo "The command you called requires the Haskell Tool Stack"
@echo "See: https://docs.haskellstack.org/en/stable/install_and_upgrade/"
@exit 1
endif endif
.PHONY: setup-check-npm
setup-check-npm:
ifeq (,$(wildcard $(shell which npm)))
@echo "The command you called requires the Node Package Manager"
@echo "See: https://www.npmjs.com/get-npm"
@exit 1
endif
.PHONY: setup-check-gem
setup-check-gem:
ifeq (,$(wildcard $(shell which gem)))
@echo "The command you called requires the RubyGems Package Manager"
@echo "See: https://www.ruby-lang.org/en/documentation/installation/"
@exit 1
endif
.PHONY: setup-check-fix-whitespace
setup-check-fix-whitespace: setup-check-stack
ifeq (,$(wildcard $(shell which fix-whitespace)))
@echo "The command you called requires fix-whitespace"
@echo "Run: git clone https://github.com/agda/fix-whitespace"
@echo " cd fix-whitespace/"
@echo " stack install --stack-yaml stack-8.8.3.yaml"
endif
.PHONY: setup-check-epubcheck
setup-check-epubcheck:
ifeq (,$(wildcard $(shell which epubcheck)))
@echo "The command you called requires EPUBCheck"
@echo "See: https://github.com/w3c/epubcheck"
endif
.PHONY: setup-install-htmlproofer
setup-install-htmlproofer: setup-check-gem
ifeq (,$(wildcard $(shell which htmlproofer)))
@echo "Installing HTMLProofer..."
gem install html-proofer
endif
.PHONY: setup-install-bundler
setup-install-bundler: setup-check-gem
ifeq (,$(wildcard $(shell which bundle)))
@echo "Installing Ruby Bundler..."
gem install bundle
endif
#################################################################################
# Build legacy versions of website using Jekyll
#################################################################################
LEGACY_VERSIONS := 19.08 20.07
LEGACY_VERSION_DIRS := $(addprefix versions/,$(addsuffix /,$(LEGACY_VERSIONS)))
legacy-versions: setup-install-bundle $(LEGACY_VERSION_DIRS)
ifeq ($(shell sed --version >/dev/null 2>&1; echo $$?),1) ifeq ($(shell sed --version >/dev/null 2>&1; echo $$?),1)
SEDI := sed -i "" SEDI := sed -i ""
else else
SEDI := sed -i SEDI := sed -i
endif endif
define build_legacy_version
# Configure the repository to use .githooks
init:
git config core.hooksPath .githooks
# Build PLFA web version and test links
default: test
# Start Jekyll server with --incremental
serve:
$(JEKYLL) serve --incremental
# Start detached Jekyll server
server-start:
$(JEKYLL) serve --no-watch --detach
# Stop detached Jekyll server
server-stop:
pkill -f jekyll
.phony: serve server-start server-stop
# Build PLFA web version using Jekyll
build: $(MARKDOWN_FILES)
$(JEKYLL) build
# Build PLFA web version using Jekyll with --incremental
build-incremental: $(MARKDOWN_FILES)
$(JEKYLL) build --incremental
# Download PLFA web releases
build-history: latest/ $(RELEASES)
latest/: $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(LATEST_VERSION)))
cd $< \
&& $(JEKYLL) clean \
&& $(JEKYLL) build --destination '../../latest' --baseurl '/latest'
# Download PLFA web release and build it under the relevant folder
define build_release
version := $(1) version := $(1)
out := $(addsuffix /,$(1)) out := $(addsuffix /,$(1))
url := $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) url := $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1)))
tmp_zip := $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) tmp_zip := $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1)))
tmp_dir := $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) tmp_dir := $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1)))
baseurl := $(addprefix /,$(1)) baseurl := $(addprefix /,$(1))
$$(tmp_zip): tmp_zip = $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) $$(tmp_zip): tmp_zip = $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1)))
$$(tmp_zip): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) $$(tmp_zip): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1)))
$$(tmp_zip): $$(tmp_zip):
@mkdir -p .versions/ @mkdir -p versions/
wget -c $$(url) -O $$(tmp_zip) @wget -c $$(url) -O $$(tmp_zip)
$$(tmp_dir): version = $(1) $$(tmp_dir): version = $(1)
$$(tmp_dir): tmp_dir = $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) $$(tmp_dir): tmp_dir = $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1)))
$$(tmp_dir): tmp_zip = $(addprefix .versions/plfa.github.io-web-,$(addsuffix .zip,$(1))) $$(tmp_dir): tmp_zip = $(addprefix versions/plfa.github.io-web-,$(addsuffix .zip,$(1)))
$$(tmp_dir): $$(tmp_zip) $$(tmp_dir): $$(tmp_zip)
yes | unzip -qq $$(tmp_zip) -d .versions/ @yes | unzip -qq $$(tmp_zip) -d versions/
$(SEDI) "s/branch: dev/branch: dev-$$(version)/" $$(addsuffix _config.yml,$$(tmp_dir)) @$(SEDI) "s/branch: dev/branch: dev-$$(version)/" $$(addsuffix _config.yml,$$(tmp_dir))
$$(out): out = $(addsuffix /,$(1)) versions/$$(out): out = $(addsuffix /,$(1))
$$(out): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1))) versions/$$(out): url = $(addprefix https://github.com/plfa/plfa.github.io/archive/web-,$(addsuffix .zip,$(1)))
$$(out): tmp_dir = $(addprefix .versions/plfa.github.io-web-,$(addsuffix /,$(1))) versions/$$(out): tmp_dir = $(addprefix versions/plfa.github.io-web-,$(addsuffix /,$(1)))
$$(out): baseurl = $(addprefix /,$(1)) versions/$$(out): baseurl = $(addprefix /,$(1))
$$(out): $$(tmp_dir) versions/$$(out): $$(tmp_dir)
cd $$(tmp_dir) \ @echo "source \"https://rubygems.org\"\n\ngroup :jekyll_plugins do\n gem 'github-pages'\nend" > $$(tmp_dir)/Gemfile
@cd $$(tmp_dir) \
&& rm -rf _posts \ && rm -rf _posts \
&& $(JEKYLL) clean \ && bundle install \
&& $(JEKYLL) build --destination '../../$$(out)' --baseurl '$$(baseurl)' && bundle exec jekyll clean \
&& bundle exec jekyll build --destination '../$$(out)' --baseurl '$$(baseurl)'
endef endef
# Incorporate previous releases of PLFA web version $(foreach legacy_version,$(LEGACY_VERSIONS),$(eval $(call build_legacy_version,$(legacy_version))))
$(foreach release_version,$(RELEASE_VERSIONS),$(eval $(call build_release,$(release_version))))
# Convert literal Agda to Markdown using highlight.sh
define AGDA_template
in := $(1)
out := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
$$(out) : in = $(1)
$$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
$$(out) : $$(in)
@echo "Processing $$(subst ./,,$$(in))"
@mkdir -p out/
ifeq (,$$(findstring courses/,$$(in)))
./highlight.sh $$(subst ./,,$$(in)) --include-path=src/
else
# Fix links to the file itself (out/<filename> to out/<filepath>)
./highlight.sh $$(subst ./,,$$(in)) --include-path=src/ --include-path=$$(subst ./,,$$(dir $$(in)))
endif
endef
$(foreach agda,$(AGDA_FILES),$(eval $(call AGDA_template,$(agda))))
.phony: build build-incremental
# Test links using htmlproofer
test: build
$(HTMLPROOFER) '_site'
# Test local links using htmlproofer
test-offline: build
$(HTMLPROOFER) '_site' --disable-external
# Test local links for stability under different base URLs
test-stable-offline: $(MARKDOWN_FILES)
$(JEKYLL) clean
$(JEKYLL) build --destination '_site/stable' --baseurl '/stable'
$(HTMLPROOFER) '_site' --disable-external
.phony: test test-offline test-stable-offline
# Build EPUB using Pandoc
epub: out/epub/plfa.epub
# Test EPUB using EPUBCheck
epubcheck: out/epub/plfa.epub
$(EPUBCHECK) out/epub/plfa.epub
out/epub/plfa.epub: $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledgements.md
@mkdir -p out/epub/
$(PANDOC) --strip-comments \
--css=epub/main.css \
--epub-embed-font='assets/fonts/mononoki.woff' \
--epub-embed-font='assets/fonts/FreeMono.woff' \
--epub-embed-font='assets/fonts/DejaVuSansMono.woff' \
--lua-filter epub/include-files.lua \
--lua-filter epub/rewrite-links.lua \
--lua-filter epub/rewrite-html-ul.lua \
--lua-filter epub/default-code-class.lua -M default-code-class=agda \
--standalone \
--fail-if-warnings \
--toc --toc-depth=2 \
--epub-chapter-level=2 \
-o "$@" \
epub/index.md
out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
@mkdir -p out/epub/
$(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@
.phony: epub epubcheck
# Clean auxiliary files
clean:
rm -f .agda-stdlib.sed .links-*.sed out/epub/acknowledgements.md
rm -rf .versions
ifneq ($(strip $(AGDAI_FILES)),)
rm $(AGDAI_FILES)
endif
# Clean generated files
clobber: clean
$(JEKYLL) clean
rm -rf out/
rm -rf latest/ $(RELEASES)
.phony: clean clobber
# Setup Travis
travis-setup:\
travis-install-agda\
travis-install-agda-stdlib\
travis-install-acknowledgements
.phony: travis-setup
# Setup Agda
travis-install-agda:\
$(HOME)/.local/bin/agda\
$(HOME)/.agda/defaults\
$(HOME)/.agda/libraries
$(HOME)/.agda/defaults:
echo "standard-library" >> $(HOME)/.agda/defaults
echo "plfa" >> $(HOME)/.agda/defaults
$(HOME)/.agda/libraries:
echo "$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/standard-library.agda-lib" >> $(HOME)/.agda/libraries
echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
$(HOME)/.local/bin/agda:
curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\
-o $(HOME)/agda-$(AGDA_VERSION).zip
unzip -qq $(HOME)/agda-$(AGDA_VERSION).zip -d $(HOME)
cd $(HOME)/agda-$(AGDA_VERSION);\
stack install --stack-yaml=stack-$(GHC_VERSION).yaml
travis-uninstall-agda:
rm -rf $(HOME)/agda-$(AGDA_VERSION)/
rm -f $(HOME)/.local/bin/agda
rm -f $(HOME)/.local/bin/agda-mode
travis-reinstall-agda: travis-uninstall-agda travis-install-agda
.phony: travis-install-agda travis-uninstall-agda travis-reinstall-agda
# Setup Agda Standard Library
travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\
-o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME)
mkdir -p $(HOME)/.agda
travis-uninstall-agda-stdlib:
rm $(HOME)/.agda/defaults
rm $(HOME)/.agda/libraries
rm -rf $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/
travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub
# Setup Acknowledgements
travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
$(HOME)/.local/bin/acknowledgements:
curl -L https://github.com/plfa/acknowledgements/archive/master.zip\
-o $(HOME)/acknowledgements-master.zip
unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
cd $(HOME)/acknowledgements-master;\
stack install
travis-uninstall-acknowledgements:
rm -rf $(HOME)/acknowledgements-master/
rm $(HOME)/.local/bin/acknowledgements
travis-reinstall-acknowledgements: travis-uninstall-acknowledgements travis-reinstall-acknowledgements
.phony: travis-install-acknowledgements travis-uninstall-acknowledgements travis-reinstall-acknowledgements

377
README.md
View file

@ -1,10 +1,13 @@
--- ---
layout: page layout : page
title: Getting Started title : Getting Started
permalink: /GettingStarted/ prev : /Preface/
permalink : /GettingStarted/
next : /Naturals/
--- ---
<!-- Status & Version Badges --> <!-- Status & Version Badges -->
[![Calendar Version][plfa-calver]][plfa-latest] [![Calendar Version][plfa-calver]][plfa-latest]
[![Build Status][plfa-status]][plfa-travis] [![Build Status][plfa-status]][plfa-travis]
[![Agda][agda-version]][agda] [![Agda][agda-version]][agda]
@ -12,19 +15,46 @@ permalink: /GettingStarted/
## Dependencies for users ## Dependencies for users
You can read PLFA [online][plfa] without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:
You can read PLFA [online][plfa] without installing anything. - [Stack](#install-the-haskell-tool-stack)
However, if you wish to interact with the code or complete the exercises, you need several things: - [Git](#install-git)
- [Agda](#install-agda-using-stack)
- [Agda][agda] - [Agda standard library](#install-plfa-and-the-agda-standard-library)
- [Agda standard library][agda-stdlib] - [PLFA](#install-plfa-and-the-agda-standard-library)
- [PLFA][plfa-dev]
PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems. PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.
### Installing Agda using Stack There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out-of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, its important to have the specific versions of Agda and the standard library shown above.
The easiest way to install any specific version of Agda is using [Stack][haskell-stack]. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda]:
### On macOS: Install the XCode Command Line Tools
On macOS, youll need to install the [XCode Command Line Tools][xcode]. For most versions of macOS, you can install these by running the following command:
```bash
xcode-select --install
```
### Install the Haskell Tool Stack
Agda is written in Haskell, so to install it well need the *Haskell Tool Stack*, or *Stack* for short. Stack is a program for managing different Haskell compilers and packages:
- *On UNIX and macOS.* Your package manager has a package for Stack, thats probably your easiest option. For instance, Homebrew on macOS and APT on Debian offer the “haskell-stack” package. Otherwise, you can follow the instructions on [the Stack website][haskell-stack]. Usually, Stack installs binaries at “~/.local/bin”. Please ensure this is on your PATH, by including the following in your shell configuration, e.g., in `~/.bash_profile`:
```bash
export PATH="${HOME}/.local/bin:${PATH}"
```
Finally, ensure that youve got the latest version of Stack, by running:
```bash
stack upgrade
```
- *On Windows.* There is a Windows installer on [the Stack website][haskell-stack].
### Install Git
If you do not already have Git installed, see [the Git downloads page][git].
### Install Agda using Stack
The easiest way to install a *specific version* of Agda is using [Stack][haskell-stack]. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda]:
```bash ```bash
git clone https://github.com/agda/agda.git git clone https://github.com/agda/agda.git
cd agda cd agda
@ -34,45 +64,147 @@ To install Agda, run Stack from the Agda source directory:
```bash ```bash
stack install --stack-yaml stack-8.8.3.yaml stack install --stack-yaml stack-8.8.3.yaml
``` ```
If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run: *This step will take a long time and a lot of memory to complete.*
#### Using an existing installation of GHC
Stack is perfectly capable of installing and managing versions of the [Glasgow Haskell Compiler][haskell-ghc] for you. However, if you already have a copy of GHC installed, and you want Stack to use your system installation, you can pass the `--system-ghc` flag and select the appropriate “stack-*.yaml” file. For instance, if you have GHC 8.2.2 installed, run:
```bash ```bash
stack install --system-ghc --stack-yaml stack-8.2.2.yaml stack install --system-ghc --stack-yaml stack-8.2.2.yaml
``` ```
### Installing the Standard Library and PLFA #### Check if Agda was installed correctly
If youd like, you can test to see if youve installed Agda correctly. Create a file called “hello.agda” with these lines:
```agda
data Greeting : Set where
hello : Greeting
You can get the required version of the Agda standard library from GitHub, either by cloning the repository and switching to the correct branch, or by downloading [the zip archive][agda-stdlib]: greet : Greeting
greet = hello
```
From a command line, change to the same directory where your “hello.agda” file is located. Then run:
```bash ```bash
git clone https://github.com/agda/agda-stdlib.git agda -v 2 hello.agda
```
You should see a short message like the following, but no errors:
```
Checking hello (/path/to/hello.agda).
Finished hello.
```
### Install PLFA and the Agda standard library
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
```bash
git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa
```
PLFA ships with the required version of the Agda standard library, so if you cloned with the `--recurse-submodules` flag, youve already got, in the “standard-library” directory!
If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that!
```bash
cd plfa/
git submodule update --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
git clone https://github.com/agda/agda-stdlib.git agda-stdlib
cd agda-stdlib cd agda-stdlib
git checkout v1.3 git checkout v1.3
``` ```
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]: Finally, we need to let Agda know where to find the Agda standard library.
```bash You'll need the path where you installed the standard library, which well refer to as “AGDA_STDLIB”. Check to see that the file “AGDA_STDLIB/standard-library.agda-lib” exists.
git clone https://github.com/plfa/plfa.github.io You will need to create two configuration files in “AGDA_DIR”. On UNIX and macOS, “AGDA_DIR” defaults to “~/.agda”. On Windwos, “AGDA_DIR” usually defaults to “%AppData%\agda”, where “%AppData%” usually defaults to “C:\Users\USERNAME\AppData\Roaming”.
- If the “AGDA_DIR” directory does not already exist, create it.
- In “AGDA_DIR”, create a plain-text file called “libraries” containing the path “AGDA_STDLIB/standard-library.agda-lib”. This lets Agda know that an Agda library called “standard-library” is available, at the path “AGDA_STDLIB”.
- In “AGDA_DIR”, create a plain-text file called “defaults” containing *just* the line “standard-library”.
More information about placing the standard libraries is available from [the Library Management page][agda-docs-package-system] of the Agda documentation.
It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the “courses” folder, or to import modules from the book, you need to do this. To do so, add the path to “plfa.agda-lib” to “~/.agda/libraries” and add “plfa” to “~/.agda/defaults”, each on a line of their own.
#### Check if the Agda standard library was installed correctly
If youd like, you can test to see if youve installed the Agda standard library correctly. Create a file called “nats.agda” with these lines:
```agda
open import Data.Nat
ten :
ten = 10
``` ```
Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions [here][agda-docs-package-system]. (Note that the is a Unicode character, not a plain capital N. You should be able to just copy-and-paste it from this page into your file.)
It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the `courses` folder, or to import modules from the book, you need to do this. To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own. From a command line, change to the same directory where your “nats.agda” file is located. Then run:
```bash
agda -v 2 nats.agda
```
You should see a several lines describing the files which Agda loads while checking your file, but no errors:
```
Checking nats (/path/to/nats.agda).
Loading Agda.Builtin.Equality (…).
Loading Data.Nat (…).
Finished nats.
```
## Setting up and using Emacs ## Setting up an editor for Agda
The recommended editor for Agda is Emacs with `agda-mode`. Agda ships with `agda-mode`, so if youve installed Agda, all you have to do to configure `agda-mode` is run: ### Emacs
The recommended editor for Agda is Emacs. To install Emacs:
- *On UNIX*, the version of Emacs in your repository is probably fine as long as it is fairly recent. There are also links to the most recent release on the [GNU Emacs downloads page][emacs].
- *On MacOS*, [Aquamacs][aquamacs] is probably the preferred version of Emacs, but GNU Emacs can also be installed via Homebrew or MacPorts. See the [GNU Emacs downloads page][emacs] for instructions.
- *On Windows*. See the [GNU Emacs downloads page][emacs] for instructions.
Make sure that you are able to open, edit, and save text files with your installation. The [tour of Emacs][emacstour] page on the GNU Emacs site describes how to access the tutorial within your Emacs installation.
Agda ships with the editor support for Emacs built-in, so if youve installed Agda, all you have to do to configure Emacs is run:
```bash ```bash
agda-mode setup agda-mode setup
agda-mode compile
```
If you are already an Emacs user and have customized your setup, you may want to note the configuration which the `setup` appends to your `.emacs` file, and integrate it with your own preferred setup.
#### Check if “agda-mode” was installed correctly
Open the `nats.agda` file you created earlier, and load and type-check the file by typing [`C-c C-l`][agda-docs-emacs-notation].
#### Auto-loading “agda-mode” in Emacs
Since version 2.6.0, Agda has had support for literate editing with Markdown, using the “.lagda.md” extension. One issue is that Emacs will default to Markdown editing mode for files with a “.md” suffix. In order to have “agda-mode” automatically loaded whenever you open a file ending with “.agda” or “.lagda.md”, add the following line to your Emacs configuration file:
```elisp
;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
(append
'(("\\.agda\\'" . agda2-mode)
("\\.lagda.md\\'" . agda2-mode))
auto-mode-alist))
```
If you already have settings which change your “auto-mode-alist” in your configuration, put these *after* the ones you already have or combine them if you are comfortable with Emacs Lisp. The configuration file for Emacs is normally located in “~/.emacs” or “~/.emacs.d/init.el”, but Aquamacs users might need to move their startup settings to the “Preferences.el” file in “~/Library/Preferences/Aquamacs Emacs/Preferences”.
#### Optional: using the “mononoki” font with Emacs
Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommend [mononoki][font-mononoki], fonts such as [Source Code Pro][font-sourcecodepro], [DejaVu Sans Mono][font-dejavusansmono], and [FreeMono][font-freemono] are all good alternatives.
You can download and install mononoki directly from [GitHub][mononoki]. For most systems, installing a font is merely a matter of clicking the downloaded “.otf” or “.ttf” file. If your package manager offers a package for mononoki, that might be easier. For instance, Homebrew on macOS offers the “font-mononoki” package, and APT on Debian offers the [“fonts-mononoki” package][font-mononoki-debian]. To configure Emacs to use mononoki as its default font, add the following to the end of your Emacs configuration file:
``` elisp
;; default to mononoki
(set-face-attribute 'default nil
:family "mononoki"
:height 120
:weight 'normal
:width 'normal)
``` ```
#### Using “agda-mode” in Emacs
To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation]. To load and type-check the file, use [`C-c C-l`][agda-docs-emacs-notation].
Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using `C-c C-l`, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole: Agda is edited interactively, using [“holes”][agda-docs-holes], which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using “C-c C-l”, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:
- `C-c C-c x`: **c**ase split on variable x - `C-c C-c x`: **c**ase split on variable x
- `C-c C-space`: fill in hole - `C-c C-space`: fill in hole
- `C-c C-r`: **r**efine with constructor - `C-c C-r`: **r**efine with constructor
- `C-c C-a`: **a**utomatically fill in hole - `C-c C-a`: **a**utomatically fill in hole
- `C-c C-,`: goal type and context - `C-c C-,`: goal type and context
- `C-c C-.`: goal type, context, and inferred type - `C-c C-.`: goal type, context, and inferred type
See [the emacs-mode docs][agda-docs-emacs-mode] for more details. See [the emacs-mode docs][agda-docs-emacs-mode] for more details.
@ -86,47 +218,40 @@ If you want to see messages beside rather than below your Agda code, you can do
Now, error messages from Agda will appear next to your file, rather than squished beneath it. Now, error messages from Agda will appear next to your file, rather than squished beneath it.
#### Entering Unicode characters in Emacs with “agda-mode”
When you write Agda code, you will need to insert characters which are not found on standard keyboards. Emacs “agda-mode” makes it easier to do this by defining character translations: when you enter certain sequences of ordinary characters (the kind you find on any keyboard), Emacs will replace them in your Agda file with the corresponding special character.
### Auto-loading `agda-mode` in Emacs For example, we can add a comment line to one of the “.agda” test files. Let's say we want to add a comment line that reads:
Since version 2.6.0, Agda has support for literate editing with Markdown, using the `.lagda.md` extension. One side-effect of this extension is that most editors default to Markdown editing mode, whereas
In order to have `agda-mode` automatically loaded whenever you open a file ending with `.agda` or `.lagda.md`, put the following on your Emacs configuration file:
```elisp
(setq auto-mode-alist
(append
'(("\\.agda\\'" . agda2-mode)
("\\.lagda.md\\'" . agda2-mode))
auto-mode-alist))
``` ```
{- I am excited to type ∀ and → and ≤ and ≡ !! -}
(The configuration file for Emacs is normally located in `~/.emacs` or `~/.emacs.d/init.el`, but Aquamacs users might need to move their startup settings to the `Preferences.el` file in `~/Library/Preferences/Aquamacs Emacs/Preferences`.)
### Using mononoki in Emacs
It is recommended that you install the font [mononoki][mononoki], and add the following to the end of your emacs configuration file at `~/.emacs`:
``` elisp
;; default to mononoki
(set-face-attribute 'default nil
:family "mononoki"
:height 120
:weight 'normal
:width 'normal)
``` ```
The first few characters are ordinary, so we would just type them as usual:
```
{- I am excited to type
```
But after that last space, we do not find ∀ on the keyboard. The code for this character is the four characters `\all`, so we type those four characters, and when we finish, Emacs will replace them with what we want:
```
{- I am excited to type ∀
```
We can continue with the codes for the other characters. Sometimes the characters will change as we type them, because a prefix of our character's code is the code of another character. This happens with the arrow, whose code is `\->`. After typing `\-` we see:
```
{- I am excited to type ∀ and
```
because the code `\-` corresponds to a hyphen of a certain width. When we add the `>`, the `­` becomes `→`! The code for `≤` is `\<=`, and the code for `≡` is `\==`.
```
{- I am excited to type ∀ and → and ≤ and ≡
```
Finally the last few characters are ordinary again,
```
{- I am excited to type ∀ and → and ≤ and ≡ !! -}
```
If you're having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the Unicode characters introduced in that chapter.
Emacs with “agda-mode” offers a number of useful commands, and two of them are especially useful when it comes to working with Unicode characters. For a full list of supported characters, use “agda-input-show-translations” with:
### Unicode characters
If you're having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the unicode characters introduced in that chapter.
`agda-mode` and emacs have a number of useful commands. Two of them are especially useful when you solve exercises.
For a full list of supported characters, use `agda-input-show-translations` with:
M-x agda-input-show-translations M-x agda-input-show-translations
All the supported characters in `agda-mode` are shown. All the supported characters in “agda-mode” are shown.
If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command: If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:
@ -136,86 +261,60 @@ You'll see the key sequence of the character in mini buffer.
## Dependencies for developers ## Dependencies for developers
PLFA is written in literate Agda with [Pandoc Markdown][pandoc].
PLFA is available as both a website and an EPUB e-book, both of which can be built on UNIX and macOS.
Finally, to help developers avoid common mistakes, we provide a set of Git hooks.
PLFA is available as both a website and an EPUB e-book, both of which can be built on Linux and macOS.
PLFA is written in literate Agda with [Kramdown Markdown][kramdown]. ### Building the website and e-book
If youd like to build the web version of PLFA locally, [Stack](#install-the-haskell-tool-stack) is all you need! PLFA is built using [Hakyll][hakyll], a Haskell library for building static websites. Weve setup a Makefile to help you run common tasks. For instance, to build PLFA, run:
```bash
make build
```
If youd like to serve PLFA locally, rebuilding the website when any of the source files are changed, run:
```bash
make watch
```
The Makefile offers more than just building and watching, it also offers the following useful options:
```
build # Build PLFA
watch # Build and serve PLFA, monitor for changes and rebuild
test # Test web version for broken links, invalid HTML, etc.
test-epub # Test EPUB for compliance to the EPUB3 standard
clean # Clean PLFA build
init # Setup the Git hooks (see below)
update-contributors # Pull in new contributors from GitHub to contributors/
list # List all build targets
```
For completeness, the Makefile also offers the following options, but youre unlikely to need these:
```
legacy-versions # Build legacy versions of PLFA
setup-install-bundler # Install Ruby Bundler (needed for legacy-versions)
setup-install-htmlproofer # Install HTMLProofer (needed for test and Git hooks)
setup-check-fix-whitespace # Check to see if fix-whitespace is installed (needed for Git hooks)
setup-check-epubcheck # Check to see if epubcheck is installed (needed for EPUB tests)
setup-check-gem # Check to see if RubyGems is installed
setup-check-npm # Check to see if the Node Package Manager is installed
setup-check-stack # Check to see if the Haskell Tool Stack is installed
```
The [EPUB version][epub] of the book is built as part of the website, since its hosted on the website.
### Git hooks ### Git hooks
The repository comes with several Git hooks: The repository comes with several Git hooks:
1. The [fix-whitespace][fix-whitespace] program is run to check for whitespace violations. 1. The [fix-whitespace][fix-whitespace] program is run to check for whitespace violations.
2. The test suite is run to check if everything type checks. 2. The test suite is run to check if everything type checks.
You can install these Git hooks by calling `make init`. You can install these Git hooks by calling “make init”.
You can install [fix-whitespace][fix-whitespace] by running: You can install [fix-whitespace][fix-whitespace] by running:
```bash ```bash
git clone https://github.com/agda/fix-whitespace git clone https://github.com/agda/fix-whitespace
cd fix-whitespace/ cd fix-whitespace/
stack install --stack-yaml stack-8.8.3.yaml stack install --stack-yaml stack-8.8.3.yaml
``` ```
If you want Stack to use your system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file, like when installing [Agda](#installing-agda-using-stack). If you want Stack to use your system installation of GHC, follow the instructions for [Using an existing installation of GHC](#using-an-existing-installation-of-ghc).
### Building the website
The website version of the book is built in three stages:
1. The `.lagda.md` files are compiled to Markdown using Agdas highlighter.
(This requires several POSIX tools, such as `bash`, `sed`, and `grep`.)
2. The Markdown files are converted to HTML using [Jekyll][ruby-jekyll], a widely-used static site builder.
(This requires [Ruby][ruby] and [Jekyll][ruby-jekyll].)
3. The HTML is checked using [html-proofer][ruby-html-proofer].
(This requires [Ruby][ruby] and [html-proofer][ruby-html-proofer].)
Most recent versions of [Ruby][ruby] should work. The easiest way to install [Jekyll][ruby-jekyll] and [html-proofer][ruby-html-proofer] is using [Bundler][ruby-bundler]. You can install [Bundler][ruby-bundler] by running:
```bash
gem install bundler
```
You can install the remainder of the dependencies—[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*—by running:
```bash
bundle install
```
Once you have installed all of the dependencies, you can build a copy of the book, and host it locally, by running:
```bash
make build
make serve
```
The Makefile offers more than just these options:
```bash
make # see make test
make build # builds lagda->markdown and the website
make build-incremental # builds lagda->markdown and the website incrementally
make test # checks all links are valid
make test-offline # checks all links are valid offline
make serve # starts the server
make server-start # starts the server in detached mode
make server-stop # stops the server, uses pkill
make clean # removes all ~unnecessary~ generated files
make clobber # removes all generated files
```
If you simply wish to have a local copy of the book, e.g. for offline reading, but don't care about editing and rebuilding the book, you can grab a copy of the [master branch][plfa-master], which is automatically built using Travis. You will still need [Jekyll][ruby-jekyll] and preferably [Bundler][ruby-bundler] to host the book (see above). To host the book this way, download a copy of the [master branch][plfa-master], unzip, and from within the directory run
```bash
bundle install
bundle exec jekyll serve
```
### Building the EPUB
The [EPUB version][epub] of the book is built using Pandoc.
Install a recent version of Pandoc, [available here][pandoc]. The easiest way to install Pandoc is using their official installer, which is much faster than compiling Pandoc from source with Haskell Stack.
Once youve installed Pandoc, you can build the EPUB by running:
```bash
make epub
```
The EPUB is written to `out/epub/plfa.epub`.
<!-- Links --> <!-- Links -->
@ -227,29 +326,31 @@ The EPUB is written to `out/epub/plfa.epub`.
[plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda [plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda
[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest [plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip [plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
[git]: https://git-scm.com/downloads
[agda]: https://github.com/agda/agda/releases/tag/v2.6.1 [agda]: https://github.com/agda/agda/releases/tag/v2.6.1
[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg [agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
[agda-docs-holes]: https://agda.readthedocs.io/en/v2.5.4/getting-started/quick-guide.html [agda-docs-holes]: https://agda.readthedocs.io/en/v2.5.4/getting-started/quick-guide.html
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html [agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations [agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library [agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
[emacs]: https://www.gnu.org/software/emacs/download.html
[emacstour]: https://www.gnu.org/software/emacs/tour/
[aquamacs]: http://aquamacs.org/
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg [agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3 [agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
[fix-whitespace]: https://github.com/agda/fix-whitespace [fix-whitespace]: https://github.com/agda/fix-whitespace
[mononoki]: https://madmalik.github.io/mononoki/
[ruby]: https://www.ruby-lang.org/en/documentation/installation/ [ruby]: https://www.ruby-lang.org/en/documentation/installation/
[ruby-bundler]: https://bundler.io/#getting-started [ruby-bundler]: https://bundler.io/#getting-started
[ruby-jekyll]: https://jekyllrb.com/ [ruby-jekyll]: https://jekyllrb.com/
[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer [ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
[hakyll]: https://jaspervdj.be/hakyll/
[kramdown]: https://kramdown.gettalong.org/syntax.html
[pandoc]: https://pandoc.org/installing.html [pandoc]: https://pandoc.org/installing.html
[epubcheck]: https://github.com/w3c/epubcheck [epubcheck]: https://github.com/w3c/epubcheck
[xcode]: https://developer.apple.com/xcode/
[font-sourcecodepro]: https://github.com/adobe-fonts/source-code-pro
[font-dejavusansmono]: https://dejavu-fonts.github.io/
[font-freemono]: https://www.gnu.org/software/freefont/
[font-mononoki]: https://madmalik.github.io/mononoki/
[font-mononoki-debian]: https://packages.debian.org/sid/fonts/fonts-mononoki

23
TODO.md Normal file
View file

@ -0,0 +1,23 @@
# Roadmap
Heres what still needs to happen in order to use Hakyll for PLFA builds.
We can release after the first milestone.
The goals in the second milestone are optional, but nice.
## Milestone 1
- migrate EPUB generation over to site.hs
## Milestone 2
- automatically generate Unicode sections
+ use a context field similar to the teaser context
+ create a template for book chapters which uses said field
+ use book chapter template for .lagda.md files
- automatically generate Statistics chapter
+ see https://github.com/plfa/plfa.github.io/blob/41939ad0312b6012ac76f056c6da1f9ff590c040/hs/agda-count.hs
- …

View file

@ -1,71 +0,0 @@
title: >
Programming Language Foundations in Agda
description: >
Programming Language Foundations in Agda
license: Creative Commons Attribution 4.0 International License
license-file: https://creativecommons.org/licenses/by/4.0/
# To include a new author, add them below in the order in which they are to be
# displayed in the author list. If they have made contributions as an author via
# GitHub, their username MUST be included in the list.
authors:
- name: Philip Wadler
email: wadler@inf.ed.ac.uk
corresponding: true
github_username: wadler
- name: Wen Kokke
email: wen.kokke@ed.ac.uk
corresponding: true
github_username: wenkokke
twitter_username: wenkokke
- name: Jeremy G. Siek
email: jsiek@indiana.edu
corresponding: true
github_username: jsiek
twitter_username: jeremysiek
extra_contributors:
- github_username: cyberglot
- name: Vikraman Choudhury
- name: Ben Darwin
- github_username: koo5
- name: Anish Tondwalkar
- name: Nils Anders Danielsson
- name: Miëtek Bak
- name: Gergő Érdi
- name: Adam Sandberg Eriksson
- name: David Janin
- name: András Kovács
- name: Ulf Norell
- name: Liam O'Connor
- name: N. Raghavendra
- name: Roman Kireev
- name: Amr Sabry
google_analytics: "UA-125055580-1"
repository: plfa/plfa.github.io
branch: dev
baseurl: ""
url: "https://plfa.github.io"
markdown: kramdown
theme: minima
excerpt_separator: <!--more-->
exclude:
- "*.lagda.md"
- "*.agdai"
- "*.agda-lib"
- "extra/"
- "papers/"
- "vendor/"
- "epub/"
- ".versions/"
- "_build/"
- "Guardfile"
- "Gemfile"
- "Gemfile.lock"
- "highlight.sh"
- "out/epub/acknowledgements.md"

View file

@ -1,36 +0,0 @@
<footer class="site-footer h-card">
<data class="u-url" href="{{ "/" | relative_url }}"></data>
<div class="wrapper">
<h2 class="footer-heading">{{ site.title | escape }}</h2>
{%- for author in site.authors -%}
{%- if author.corresponding -%}
<div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">{{ author.name | escape }}</li>
<li>
{%- if author.email -%}
<a class="u-email" href="mailto:{{ author.email }}">{{ author.email }}</a>
{%- endif -%}
</li>
</ul>
</div>
<div class="footer-col footer-col-2">
{%- include social.html -%}
</div>
<div class="footer-col footer-col-3">
{%- if author.blurb -%}
<p>{{- author.blurb | escape -}}</p>
{%- endif -%}
</div>
</div>
{%- endif -%}
{%- endfor -%}
This work is licensed under a <a rel="license" href="{{ site.license-file }}">{{ site.license }}</a>
</div>
</footer>

View file

@ -1,17 +0,0 @@
<head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>
{%- if page.layout == 'home' -%}
{{ site.title }}
{%- else -%}
{{ page.title }} | {{ site.title }}
{%- endif -%}
</title>
{%- seo title=false -%}
<link rel="stylesheet" href="{{ "/assets/main.css" | relative_url }}">
{%- if jekyll.environment == 'production' and site.google_analytics -%}
{%- include google-analytics.html -%}
{%- endif -%}
</head>

View file

@ -1,17 +0,0 @@
<p style="text-align:center;">
{% if page.prev %}
<a alt="Previous chapter" href="{{ site.baseurl }}{{ page.prev }}">Prev</a>
{% endif %}
{% if page.prev and (page.src or page.next) %}
&bullet;
{% endif %}
{% if page.src %}
<a alt="Source code" href="https://github.com/{{ site.repository }}/blob/{{ site.branch }}/{{ page.src }}">Source</a>
{% endif %}
{% if page.src and page.next %}
&bullet;
{% endif %}
{% if page.next %}
<a alt="Next chapter" href="{{ site.baseurl }}{{ page.next }}">Next</a>
{% endif %}
</p>

View file

@ -1,77 +0,0 @@
<!-- Import jQuery -->
<script type="text/javascript" src="{{ "/assets/jquery.js" | prepend: site.baseurl }}"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
<script type="text/javascript">
// Add anchors on DOMContentLoaded
document.addEventListener('DOMContentLoaded', function(event) {
anchors.add();
});
</script>
<script type="text/javascript">
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="{{ "/assets/katex.js" | prepend: site.baseurl }}"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>

View file

@ -1,13 +0,0 @@
<ul class="social-media-list">
{%- if author.dribbble_username -%}<li><a href="https://dribbble.com/{{ author.dribbble_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#dribbble' | relative_url }}"></use></svg> <span class="username">{{ author.dribbble_username| escape }}</span></a></li>{%- endif -%}
{%- if author.facebook_username -%}<li><a href="https://www.facebook.com/{{ author.facebook_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#facebook' | relative_url }}"></use></svg> <span class="username">{{ author.facebook_username| escape }}</span></a></li>{%- endif -%}
{%- if author.flickr_username -%}<li><a href="https://www.flickr.com/photos/{{ author.flickr_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#flickr' | relative_url }}"></use></svg> <span class="username">{{ author.flickr_username| escape }}</span></a></li>{%- endif -%}
{%- if author.github_username -%}<li><a href="https://github.com/{{ author.github_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#github' | relative_url }}"></use></svg> <span class="username">{{ author.github_username| escape }}</span></a></li>{%- endif -%}
{%- if author.instagram_username -%}<li><a href="https://instagram.com/{{ author.instagram_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#instagram' | relative_url }}"></use></svg> <span class="username">{{ author.instagram_username| escape }}</span></a></li>{%- endif -%}
{%- if author.linkedin_username -%}<li><a href="https://www.linkedin.com/in/{{ author.linkedin_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#linkedin' | relative_url }}"></use></svg> <span class="username">{{ author.linkedin_username| escape }}</span></a></li>{%- endif -%}
{%- if author.pinterest_username -%}<li><a href="https://www.pinterest.com/{{ author.pinterest_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#pinterest' | relative_url }}"></use></svg> <span class="username">{{ author.pinterest_username| escape }}</span></a></li>{%- endif -%}
{%- for mst in author.mastodon -%}{%- if mst.username and mst.instance -%}<li><a href="https://{{ mst.instance| cgi_escape | escape}}/@{{mst.username}}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#mastodon' | relative_url }}"></use></svg> <span class="username">{{ mst.username|escape }}</span></a></li>{%- endif -%}{%- endfor -%}
{%- if author.twitter_username -%}<li><a href="https://www.twitter.com/{{ author.twitter_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#twitter' | relative_url }}"></use></svg> <span class="username">{{ author.twitter_username| escape }}</span></a></li>{%- endif -%}
{%- if author.youtube_username -%}<li><a href="https://youtube.com/{{ author.youtube_username| cgi_escape | escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#youtube' | relative_url }}"></use></svg> <span class="username">{{ author.youtube_username| escape }}</span></a></li>{%- endif -%}
{%- if author.googleplus_username -%}<li><a href="https://plus.google.com/{{ author.googleplus_username| escape }}"><svg class="svg-icon"><use xlink:href="{{ '/assets/minima-social-icons.svg#googleplus' | relative_url }}"></use></svg> <span class="username">{{ author.googleplus_username| escape }}</span></a></li>{%- endif -%}
</ul>

View file

@ -1,29 +0,0 @@
<!DOCTYPE html>
<html lang="{{ page.lang | default: site.lang | default: "en" }}">
{%- include head.html -%}
<body>
{%- include header.html -%}
<main class="page-content" aria-label="Content">
<div class="wrapper">
{{ content }}
</div>
</main>
{%- include footer.html -%}
<script type="text/javascript">
// Fix sandwich menu
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
</script>
{%- include script.html -%}
</body>
</html>

View file

@ -1,30 +0,0 @@
---
layout: default
---
<div class="home">
{{ content }}
{%- if site.posts.size > 0 -%}
<h1 class="post-list-heading">Announcements</h1>
<ul class="post-list">
{%- for post in site.posts -%}
<li>
{%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%}
<span class="post-meta">{{ post.date | date: date_format }}</span>
<h2>{{ post.title | escape }}</h2>
{%- if post.short -%}
{{ post.excerpt }}
{%- else -%}
{{ post.excerpt }}
<a href="{{ post.url | relative_url }}">(more)</a>
{%- endif -%}
</li>
{%- endfor -%}
</ul>
<p class="feed-subscribe"><svg class="svg-icon orange"><use xlink:href="{{ '/assets/minima-social-icons.svg#rss' | relative_url }}"></use></svg><a href="{{ "/feed.xml" | relative_url }}">Subscribe</a></p>
{%- endif -%}
</div>

View file

@ -1,19 +0,0 @@
---
layout: default
---
<article class="post">
<header class="post-header">
<h1 class="post-title">{{ page.title | escape }}</h1>
</header>
{% include next.html %}
<div class="post-content">
{{ content }}
</div>
{% include next.html %}
</article>

View file

@ -1,27 +0,0 @@
---
layout: default
---
<article class="post h-entry" itemscope itemtype="http://schema.org/BlogPosting">
<header class="post-header">
<h1 class="post-title p-name" itemprop="name headline">{{ page.title | escape }}</h1>
<p class="post-meta">
<time class="dt-published" datetime="{{ page.date | date_to_xmlschema }}" itemprop="datePublished">
{%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%}
{{ page.date | date: date_format }}
</time>
{%- if page.author -%}
<span itemprop="author" itemscope itemtype="http://schema.org/Person"><span class="p-author h-card" itemprop="name">{{ page.author | escape }}</span></span>
{%- endif -%}</p>
</header>
<div class="post-content e-content" itemprop="articleBody">
{{ content }}
</div>
{%- if site.disqus.shortname -%}
{%- include disqus_comments.html -%}
{%- endif -%}
<a class="u-url" href="{{ page.url | relative_url }}" hidden></a>
</article>

File diff suppressed because one or more lines are too long

View file

@ -1,28 +0,0 @@
---
# Only the main Sass file needs front matter (the dashes are enough)
---
@import "katex";
@import "minima";
@import "agda";
$on-medium: 600px !default;
.trigger { display: none; }
@media screen and (min-width: $on-medium) {
.trigger { display: block; }
}
ul.list-of-contributors {
display: grid;
grid-template-columns: repeat(3, 1fr);
width: calc(100% - 2rem);
}
ul.list-of-contributors li {
margin-right: 2rem;
}
pre {
break-inside: avoid;
}

7
authors/jsiek.metadata Normal file
View file

@ -0,0 +1,7 @@
---
name : Jeremy G. Siek
email : jsiek@indiana.edu
corresponding : true
github : jsiek
twitter : jeremysiek
---

6
authors/wadler.metadata Normal file
View file

@ -0,0 +1,6 @@
---
name : Philip Wadler
email : wadler@inf.ed.ac.uk
corresponding : true
github : wadler
---

View file

@ -0,0 +1,7 @@
---
name : Wen Kokke
email : wen.kokke@ed.ac.uk
corresponding : true
github : wenkokke
twitter : wenkokke
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Mike He
github: AD1024
---

View file

@ -0,0 +1,5 @@
---
name: András Kovács
github: AndrasKovacs
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Dee Yeum
github: ChefYeum
---

View file

@ -0,0 +1,5 @@
---
count: 12
name: Chad Nester
github: Cubesoup
---

View file

@ -0,0 +1,5 @@
---
count: 7
name: Juhana Laurinharju
github: Fingerzam
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Gagan Devagiri
github: GaganSD
---

View file

@ -0,0 +1,5 @@
---
count: 36
name: Zbigniew Stanasiuk
github: Kwezan
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Liang-Ting Chen
github: L-TChen
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Isaac Elliott
github: LightAndLight
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Matthias Gabriel
github: MatthiasGabriel
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Oling Cat
github: OlingCat
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Torsten Grust
github: Teggy
---

View file

@ -0,0 +1,5 @@
---
name: Ulf Norell
github: UlfNorell
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 4
name: Alexandru Brisan
github: abrisan
---

View file

@ -0,0 +1,5 @@
---
name: Adam Sandberg Eriksson
github: adamse
count: 1
---

View file

@ -0,0 +1,5 @@
---
name: Anish Tondwalkar
github: atondwal
count: 1
---

View file

@ -0,0 +1,5 @@
---
name: Ben Darwin
github: bcdarwin
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: caryoscelus
github: caryoscelus
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Chike Abuah
github: chikeabuah
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: citrusmunch
github: citrusmunch
---

View file

@ -0,0 +1,5 @@
---
name: April Gonçalves
github: cyberglot
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Deniz Alp
github: dalpd
---

View file

@ -0,0 +1,5 @@
---
name: David Janin
github: djanin
count: 1
---

View file

@ -0,0 +1,5 @@
---
name: Roman Kireev
github: effectfully
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 8
name: Fangyi Zhou
github: fangyi-zhou
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: G. Allais
github: gallais
---

View file

@ -0,0 +1,5 @@
---
name: Gergő Érdi
github: gergoerdi
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Georgi Lyubenov
github: googleson78
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Gan Shen
github: gshen42
---

View file

@ -0,0 +1,5 @@
---
count: 28
name: Reza Gharibi
github: h4iku
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Hugo Gualandi
github: hugomg
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Ingo Blechschmidt
github: iblech
---

View file

@ -0,0 +1,5 @@
---
count: 4
name: Jonathan Prieto
github: jonaprieto
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: John Maraist
github: jphmrst
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Kartik Singhal
github: k4rtik
---

View file

@ -0,0 +1,5 @@
---
count: 5
name: Kenichi Asai
github: kenichi-asai
---

View file

@ -0,0 +1,5 @@
---
name: koo5
github: koo5
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Stefan Kranich
github: kranich
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Kenneth MacKenzie
github: kwxm
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: James Wood
github: laMudri
---

View file

@ -0,0 +1,5 @@
---
name: Liam O'Connor
github: liamoc
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: Lorenzo Martinico
github: lzmartinico
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: Matthew Healy
github: matthew-healy
---

View file

@ -0,0 +1,5 @@
---
count: 114
name: Marko Dimjašević
github: mdimjasevic
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Merlin Göttlinger
github: mgttlinger
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: Michel Steuwer
github: michel-steuwer
---

View file

@ -0,0 +1,5 @@
---
name: Miëtek Bak
github: mietek
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Alexandre Moreno
github: moleike
---

View file

@ -0,0 +1,5 @@
---
count: 7
name: Mo Mirza
github: momirza
---

View file

@ -0,0 +1,5 @@
---
count: 19
name: Michael Reed
github: mreed20
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: Murilo Giacometti Rocha
github: murilogiacometti
---

View file

@ -0,0 +1,5 @@
---
name: Nils Anders Danielsson
github: nad
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Léo Gillot-Lamure
github: navaati
---

View file

@ -0,0 +1,5 @@
---
name: N. Raghavendra
github: nyraghu
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: bc²
github: odanoburu
---

View file

@ -0,0 +1,5 @@
---
count: 5
name: Orestis Melkonian
github: omelkonian
---

View file

@ -0,0 +1,5 @@
---
count: 4
name: Pedro Minicz
github: pedrominicz
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Peter Thiemann
github: peterthiemann
---

View file

@ -0,0 +1,5 @@
---
count: 4
name: phi16
github: phi16
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Phil de Joux
github: philderbeast
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Nathaniel Carroll
github: potato4444
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: purchan
github: purchan
---

View file

@ -0,0 +1,5 @@
---
count: 5
name: Qais Patankar
github: qaisjp
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Rodrigo Bernardo
github: rodamber
---

View file

@ -0,0 +1,5 @@
---
name: Amr Sabry
github: sabry
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Spencer Whitt
github: spwhitt
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Stephan Boyer
github: stepchowfun
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Syed Turab Ali Jafri
github: trajafri
---

View file

@ -0,0 +1,5 @@
---
name: Vikraman Choudhury
github: vikraman
count: 1
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Slava
github: vipo
---

View file

@ -0,0 +1,5 @@
---
count: 3
name: Sebastian Miele
github: whxvd
---

View file

@ -0,0 +1,5 @@
---
count: 20
name: Yasu Watanabe
github: ywata
---

View file

@ -0,0 +1,5 @@
---
count: 2
name: Zach Brown
github: zachrbrown
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Nicolas Wu
github: zenzike
---

View file

@ -0,0 +1,5 @@
---
count: 1
name: Zack Grannan
github: zgrannan
---

View file

@ -81,7 +81,7 @@ Since we define equality here, any import would create a conflict.
#### Exercise `≤-Reasoning` (stretch) #### Exercise `≤-Reasoning` (stretch)
The proof of monotonicity from The proof of monotonicity from
Chapter [Relations]({{ site.baseurl }}/Relations/) Chapter [Relations](/Relations/)
can be written in a more readable form by using an analogue of our can be written in a more readable form by using an analogue of our
notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use
it to write out an alternative proof that addition is monotonic with it to write out an alternative proof that addition is monotonic with
@ -126,8 +126,8 @@ Show that equivalence is reflexive, symmetric, and transitive.
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding} #### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
Recall that Exercises Recall that Exercises
[Bin]({{ site.baseurl }}/Naturals/#Bin) and [Bin](/Naturals/#Bin) and
[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws) [Bin-laws](/Induction/#Bin-laws)
define a datatype `Bin` of bitstrings representing natural numbers, define a datatype `Bin` of bitstrings representing natural numbers,
and asks you to define the following functions and predicates: and asks you to define the following functions and predicates:
@ -149,7 +149,7 @@ Why do `to` and `from` not form an isomorphism?
#### Exercise `⇔≃×` (recommended) #### Exercise `⇔≃×` (recommended)
Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff) Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff)
is isomorphic to `(A → B) × (B → A)`. is isomorphic to `(A → B) × (B → A)`.
``` ```
@ -221,7 +221,7 @@ Does the converse hold? If so, prove; if not, give a counterexample.
#### Exercise `<-irreflexive` (recommended) #### Exercise `<-irreflexive` (recommended)
Using negation, show that Using negation, show that
[strict inequality]({{ site.baseurl }}/Relations/#strict-inequality) [strict inequality](/Relations/#strict-inequality)
is irreflexive, that is, `n < n` holds for no `n`. is irreflexive, that is, `n < n` holds for no `n`.
``` ```
@ -232,7 +232,7 @@ is irreflexive, that is, `n < n` holds for no `n`.
#### Exercise `trichotomy` (practice) #### Exercise `trichotomy` (practice)
Show that strict inequality satisfies Show that strict inequality satisfies
[trichotomy]({{ site.baseurl }}/Relations/#trichotomy), [trichotomy](/Relations/#trichotomy),
that is, for any naturals `m` and `n` exactly one of the following holds: that is, for any naturals `m` and `n` exactly one of the following holds:
* `m < n` * `m < n`
@ -310,7 +310,7 @@ postulate
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
``` ```
Compare this with the result (`→-distrib-×`) in Compare this with the result (`→-distrib-×`) in
Chapter [Connectives]({{ site.baseurl }}/Connectives/). Chapter [Connectives](/Connectives/).
#### Exercise `⊎∀-implies-∀⊎` (practice) #### Exercise `⊎∀-implies-∀⊎` (practice)
@ -400,9 +400,9 @@ Does the converse hold? If so, prove; if not, explain why.
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism} #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
Recall that Exercises Recall that Exercises
[Bin]({{ site.baseurl }}/Naturals/#Bin), [Bin](/Naturals/#Bin),
[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and [Bin-laws](/Induction/#Bin-laws), and
[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates) [Bin-predicates](/Relations/#Bin-predicates)
define a datatype `Bin` of bitstrings representing natural numbers, define a datatype `Bin` of bitstrings representing natural numbers,
and asks you to define the following functions and predicates: and asks you to define the following functions and predicates:
@ -469,7 +469,7 @@ postulate
#### Exercise `iff-erasure` (recommended) #### Exercise `iff-erasure` (recommended)
Give analogues of the `_⇔_` operation from Give analogues of the `_⇔_` operation from
Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff), Chapter [Isomorphism](/Isomorphism/#iff),
operation on booleans and decidables, and also show the corresponding erasure: operation on booleans and decidables, and also show the corresponding erasure:
``` ```
postulate postulate

Some files were not shown because too many files have changed in this diff Show more