michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Added fix-whitespace.yaml and fixed whitespace.

Browse source
This commit is contained in:
Wen Kokke 2020-08-19 21:54:21 +02:00
parent a591bf8616
commit f06137a621
15 changed files with 173 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
LICENSE
View file

@ -33,7 +33,7 @@ exhaustive, and do not form part of our licenses.
material not subject to the license. This includes other CC- material not subject to the license. This includes other CC-
licensed material, or material used under an exception or licensed material, or material used under an exception or
limitation to copyright. More considerations for licensors: limitation to copyright. More considerations for licensors:
wiki.creativecommons.org/Considerations_for_licensors wiki.creativecommons.org/Considerations_for_licensors
Considerations for the public: By using one of our public Considerations for the public: By using one of our public
licenses, a licensor grants the public permission to use the licenses, a licensor grants the public permission to use the
@ -49,8 +49,8 @@ exhaustive, and do not form part of our licenses.
such as asking that all changes be marked or described. such as asking that all changes be marked or described.
Although not required by our licenses, you are encouraged to Although not required by our licenses, you are encouraged to
respect those requests where reasonable. More considerations respect those requests where reasonable. More considerations
for the public: for the public:
wiki.creativecommons.org/Considerations_for_licensees wiki.creativecommons.org/Considerations_for_licensees
======================================================================= =======================================================================

24
Notes.md
View file

@ -30,7 +30,7 @@ Git commands to create a branch and pull request
git branch -- list all branches git branch -- list all branches
git branch <name> -- create new local branch <name> git branch <name> -- create new local branch <name>
git checkout <name> -- make <name> the current branch git checkout <name> -- make <name> the current branch
git merge <name> -- merge branch <name> into current branch git merge <name> -- merge branch <name> into current branch
git push origin <name> -- make local branch <name> into remote git push origin <name> -- make local branch <name> into remote
On website, use pulldown menu to swith branch and then On website, use pulldown menu to swith branch and then
@ -39,9 +39,9 @@ click "new pull request" button.
## Suggestion from Conor for Inference ## Suggestion from Conor for Inference
Conor McBride <conor.mcbride@strath.ac.uk> Conor McBride <conor.mcbride@strath.ac.uk>
29 Oct 2018, 09:34 29 Oct 2018, 09:34
Hi Phil Hi Phil
In a rush, but... In a rush, but...
@ -108,11 +108,11 @@ Three possible orders:
+ (a) As current + (a) As current
+ (b) Put Lists immediately after Induction. + (b) Put Lists immediately after Induction.
- requires moving composition & extensionality earlier - requires moving composition & extensionality earlier
- requires moving parameterised modules earlier for monoids - requires moving parameterised modules earlier for monoids
- add material to relations: - add material to relations:
lexical ordering, subtype ordering, All, Any, All-++ iff lexical ordering, subtype ordering, All, Any, All-++ iff
- add material to isomorphism: All-++ isomorphism - add material to isomorphism: All-++ isomorphism
- retain material on decidability of All, Any in Decidable - retain material on decidability of All, Any in Decidable
+ (c) Put Lists after Decidable + (c) Put Lists after Decidable
- requires moving Any-decidable from Decidable to Lists - requires moving Any-decidable from Decidable to Lists
+ (d) As (b) but put parameterised modules in a separate chapter + (d) As (b) but put parameterised modules in a separate chapter
@ -121,7 +121,7 @@ Tradeoffs:
+ (b) Distribution of exercises near where material is taught + (b) Distribution of exercises near where material is taught
+ (b) Additional reinforcement for simple proofs by induction + (b) Additional reinforcement for simple proofs by induction
+ (a,c) Can drop material if there is lack of time + (a,c) Can drop material if there is lack of time
+ (a,c) Earlier emphasis on induction over evidence + (a,c) Earlier emphasis on induction over evidence
+ (c) More consistent structuring principle + (c) More consistent structuring principle
## Set up lists of exercises to do ## Set up lists of exercises to do
@ -188,9 +188,9 @@ Tradeoffs:
+ defined break, make to extract a prefix + defined break, make to extract a prefix
and count primes at end of an id. But hard and count primes at end of an id. But hard
to do corresponding proofs. Need to figure out to do corresponding proofs. Need to figure out
how to exploit abstraction to make terms readable. how to exploit abstraction to make terms readable.
+ Conversion of raw to scoped and scoped to raw + Conversion of raw to scoped and scoped to raw
is easy if I use impossible is easy if I use impossible
+ Added conversion of TypedDB to PHOAS in + Added conversion of TypedDB to PHOAS in
extra/DeBruijn-agda-list-4.lagda extra/DeBruijn-agda-list-4.lagda
+ Next: try adding bidirectional typing to + Next: try adding bidirectional typing to
@ -200,7 +200,7 @@ Tradeoffs:
+ updated Agda from: + updated Agda from:
Agda version 2.6.0-4654bfb-dirty Agda version 2.6.0-4654bfb-dirty
to: to:
Agda version 2.6.0-2f2f4f5 Agda version 2.6.0-2f2f4f5
Now TypedFresh.lagda computes 2+2 in milliseconds Now TypedFresh.lagda computes 2+2 in milliseconds
(as opposed to failing to compute it in one day). (as opposed to failing to compute it in one day).
@ -218,7 +218,7 @@ The following comments were collected on the Agda mailing list.
* Nils Anders Danielsson <nad@cse.gu.se> * Nils Anders Danielsson <nad@cse.gu.se>
+ cites Chlipala, who uses binary parametricity + cites Chlipala, who uses binary parametricity
- http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html - http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html
- http://adam.chlipala.net/cpdt/html/Intensional.html - http://adam.chlipala.net/cpdt/html/Intensional.html
* Roman <effectfully@gmail.com> * Roman <effectfully@gmail.com>
@ -228,7 +228,7 @@ The following comments were collected on the Agda mailing list.
+ also cites Abel's habilitation + also cites Abel's habilitation
- http://www.cse.chalmers.se/~abela/habil.pdf - http://www.cse.chalmers.se/~abela/habil.pdf
+ See his note to the Agda mailing list of 26 June, + See his note to the Agda mailing list of 26 June,
"Typed Jigger in vanilla Agda" "Typed Jigger in vanilla Agda"
It points to the following solution. It points to the following solution.
- https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda - https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda

83
README.md
View file

@ -4,47 +4,13 @@ title: Getting Started
permalink: /GettingStarted/ permalink: /GettingStarted/
--- ---
<!-- Links -->
[epub]: https://plfa.github.io/out/epub/plfa.epub
[plfa]: http://plfa.inf.ed.ac.uk
[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
[plfa-travis]: https://travis-ci.org/plfa/plfa.github.io
[plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda
[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
[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-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-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
[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
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
[mononoki]: https://madmalik.github.io/mononoki/
[ruby]: https://www.ruby-lang.org/en/documentation/installation/
[ruby-bundler]: https://bundler.io/#getting-started
[ruby-jekyll]: https://jekyllrb.com/
[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
[kramdown]: https://kramdown.gettalong.org/syntax.html
[pandoc]: https://pandoc.org/installing.html
[epubcheck]: https://github.com/w3c/epubcheck
<!-- 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]
[![agda-stdlib][agda-stdlib-version]][agda-stdlib] [![agda-stdlib][agda-stdlib-version]][agda-stdlib]
## Dependencies for users ## Dependencies for users
You can read PLFA [online][plfa] without installing anything. You can read PLFA [online][plfa] without installing anything.
@ -146,10 +112,10 @@ It is recommended that you install the font [mononoki][mononoki], and add the fo
``` elisp ``` elisp
;; default to mononoki ;; default to mononoki
(set-face-attribute 'default nil (set-face-attribute 'default nil
:family "mononoki" :family "mononoki"
:height 120 :height 120
:weight 'normal :weight 'normal
:width 'normal) :width 'normal)
``` ```
@ -174,8 +140,7 @@ You'll see the key sequence of the character in mini buffer.
## Dependencies for developers ## Dependencies for developers
PLFA is available as both a website and an EPUB e-book, PLFA is available as both a website and an EPUB e-book, both of which can be built on Linux and macOS.
both of which can be built on Linux and macOS.
PLFA is written in literate Agda with [Kramdown Markdown][kramdown]. PLFA is written in literate Agda with [Kramdown Markdown][kramdown].
### Building the website ### Building the website
@ -195,7 +160,7 @@ Most recent versions of [Ruby][ruby] should work. The easiest way to install [Je
```bash ```bash
gem install bundler gem install bundler
``` ```
You can install the remainder of the dependencies---[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*---by running: You can install the remainder of the dependencies—[Jekyll][ruby-jekyll], [html-proofer][ruby-html-proofer], *etc.*—by running:
```bash ```bash
bundle install bundle install
``` ```
@ -234,3 +199,37 @@ Once you’ve installed Pandoc, you can build the EPUB by running:
make epub make epub
``` ```
The EPUB is written to `out/epub/plfa.epub`. The EPUB is written to `out/epub/plfa.epub`.
<!-- Links -->
[epub]: https://plfa.github.io/out/epub/plfa.epub
[plfa]: http://plfa.inf.ed.ac.uk
[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
[plfa-travis]: https://travis-ci.org/plfa/plfa.github.io
[plfa-calver]: https://img.shields.io/badge/calver-20.07-22bfda
[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
[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-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-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
[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
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
[mononoki]: https://madmalik.github.io/mononoki/
[ruby]: https://www.ruby-lang.org/en/documentation/installation/
[ruby-bundler]: https://bundler.io/#getting-started
[ruby-jekyll]: https://jekyllrb.com/
[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
[kramdown]: https://kramdown.gettalong.org/syntax.html
[pandoc]: https://pandoc.org/installing.html
[epubcheck]: https://github.com/w3c/epubcheck

6
courses/tspl/2019/tspl2019.md
View file

@ -66,7 +66,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07.
<tr> <tr>
<td>7</td> <td>7</td>
<td><b>28 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td> <td><b>28 Oct</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
<td><b>30 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td> <td><b>30 Oct</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
<td><b>1 Nov</b> (no class) </td> <td><b>1 Nov</b> (no class) </td>
</tr> </tr>
<tr> <tr>
@ -91,7 +91,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07.
<td>11</td> <td>11</td>
<td><b>25 Nov</b> Quantitative (Wen) </td> <td><b>25 Nov</b> Quantitative (Wen) </td>
<td><b>27 Nov</b> (no class) </td> <td><b>27 Nov</b> (no class) </td>
<td><b>29 Nov</b> Mock Exam </td> <td><b>29 Nov</b> Mock Exam </td>
</tr> </tr>
</table> </table>
@ -162,7 +162,7 @@ practice for the exam and familiarise yourself with exam conditions.
* John Reynolds, * John Reynolds,
[Three Approaches to Type Structure][reynolds], [Three Approaches to Type Structure][reynolds],
_Mathematical Foundations of Software Development_, _Mathematical Foundations of Software Development_,
LNCS 185, pages 97–138, 1985. LNCS 185, pages 97–138, 1985.
* Henk Barendregt, * Henk Barendregt,
[Introduction to generalized type systems][barendregt] [Introduction to generalized type systems][barendregt]

60
fix-whitespace.yaml Normal file
View file

@ -0,0 +1,60 @@
# This file contains the project-specific settings for `fix-whitespace` a tiny
# but useful tool to
#
# * Removes trailing whitespace.
# * Removes trailing lines containing nothing but whitespace.
# * Ensures that the file ends in a newline character.
#
# By default, fix-whitespace checks every directory under the current working
# directory but no files. This program should be placed under a text-based
# project.
#
# For directories,
#
# 1) excluded-dirs is a black-list of directories,
# 2) included-dirs is a white-list of excluded-dirs
#
# For files,
#
# 3) included-files is a white-list of files,
# 4) excluded-files is a black-list of included-files.
#
# The extended glob pattern can be used to specify file/direcotory names.
# For details, see http://hackage.haskell.org/package/filemanip-0.3.6.3/docs/System-FilePath-GlobPattern.html
#
included-dirs:
- "src"
- "epub"
- "_includes"
- "_layouts"
- "_posts"
- "_sass"
- "_assets"
- "courses"
- "papers"
excluded-dirs:
- ".stack-work"
- ".git"
- "_build"
- "_site"
- "extra"
- "tmp"
# Every matched filename is included unless it is matched by excluded-files.
included-files:
- "*.md"
- "*.sh"
- "*.html"
- "*.yml"
- "*.yaml"
- "*.agda-lib"
- "Gemfile"
- "Guardfile"
- "LICENSE"
excluded-files:
- "*.sed"
- ".DS_Store"
- "Gemfile.lock"
- "Makefile"

16
papers/sbmf/Makefile
View file

@ -4,17 +4,17 @@
default : PLFA.pdf default : PLFA.pdf
PLFA.pdf : PLFA.tex PLFA.bib PLFA.pdf : PLFA.tex PLFA.bib
pdflatex PLFA pdflatex PLFA
bibtex PLFA bibtex PLFA
pdflatex PLFA pdflatex PLFA
bibtex PLFA bibtex PLFA
pdflatex PLFA pdflatex PLFA
final.zip : PLFA.tex PLFA.bib final.zip : PLFA.tex PLFA.bib
zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png
clean: clean:
rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls
realclean: clean realclean: clean
rm -f *.glob *.vo *.bbl latex/* PLFA.pdf rm -f *.glob *.vo *.bbl latex/* PLFA.pdf

16
papers/scp/Makefile
View file

@ -4,17 +4,17 @@
default : PLFA.pdf default : PLFA.pdf
PLFA.pdf : PLFA.tex PLFA.bib PLFA.pdf : PLFA.tex PLFA.bib
pdflatex PLFA pdflatex PLFA
bibtex PLFA bibtex PLFA
pdflatex PLFA pdflatex PLFA
bibtex PLFA bibtex PLFA
pdflatex PLFA pdflatex PLFA
final.zip : PLFA.tex PLFA.bib final.zip : PLFA.tex PLFA.bib
zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png
clean: clean:
rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls
realclean: clean realclean: clean
rm -f *.glob *.vo *.bbl latex/* PLFA.pdf rm -f *.glob *.vo *.bbl latex/* PLFA.pdf

2
src/plfa/acknowledgements.md
View file

@ -57,4 +57,4 @@ For support:
* EPSRC Programme Grant EP/K034413/1 * EPSRC Programme Grant EP/K034413/1
* NSF Grant No. 1814460 * NSF Grant No. 1814460
* Foundation Sciences Mathematiques de Paris (FSMP) * Foundation Sciences Mathematiques de Paris (FSMP)
Distinguised Professor Fellowship Distinguised Professor Fellowship

1
src/plfa/announcements.md
View file

@ -4,4 +4,3 @@ layout : home
permalink : /Announcements/ permalink : /Announcements/
--- ---

24
src/plfa/citing.md
View file

@ -15,13 +15,13 @@ permalink : /Citing/
### BibTeX ### BibTeX
@Book{plfa2020, @Book{plfa2020,
author = {Philip Wadler and Wen Kokke and Jeremy G. Siek}, author = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
title = {Programming Language Foundations in {A}gda}, title = {Programming Language Foundations in {A}gda},
note = {Available at \url{http://plfa.inf.ed.ac.uk/20.07/}}, note = {Available at \url{http://plfa.inf.ed.ac.uk/20.07/}},
year = 2020, year = 2020,
month = jul, month = jul,
} }
## PLFA version 19.08 ## PLFA version 19.08
@ -35,10 +35,10 @@ permalink : /Citing/
### BibTeX ### BibTeX
@Book{plfa2019, @Book{plfa2019,
author = {Philip Wadler and Wen Kokke}, author = {Philip Wadler and Wen Kokke},
title = {Programming Language Foundations in {A}gda}, title = {Programming Language Foundations in {A}gda},
note = {Available at \url{http://plfa.inf.ed.ac.uk/19.08/}}, note = {Available at \url{http://plfa.inf.ed.ac.uk/19.08/}},
year = 2019, year = 2019,
month = aug, month = aug,
} }

2
src/plfa/part1/Quantifiers.lagda.md
View file

@ -470,7 +470,7 @@ binary number `b`, there is only one proof of `One b` and similarly
for `Can b`. for `Can b`.
≡One : ∀{b : Bin} (o o' : One b) → o ≡ o' ≡One : ∀{b : Bin} (o o' : One b) → o ≡ o'
≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb' ≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb'
Many of the alternatives for proving `to∘from` turn out to be tricky. Many of the alternatives for proving `to∘from` turn out to be tricky.

2
src/plfa/part2/BigStep.lagda.md
View file

@ -293,7 +293,7 @@ below.
⟨ subst σ (ƛ N) , ⟨ subst σ (ƛ N) ∎ , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩ ⟨ subst σ (ƛ N) , ⟨ subst σ (ƛ N) ∎ , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩
⇓→—↠×≈{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ ⇓→—↠×≈{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ
with ⇓→—↠×≈{σ = σ} L⇓ƛNδ γ≈ₑσ with ⇓→—↠×≈{σ = σ} L⇓ƛNδ γ≈ₑσ
... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN ... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN
with ⇓→—↠×≈ {σ = ext-subst τ (subst σ M)} N⇓V with ⇓→—↠×≈ {σ = ext-subst τ (subst σ M)} N⇓V
(λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x}) (λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x})
| β{∅}{subst (exts τ) N}{subst σ M} | β{∅}{subst (exts τ) N}{subst σ M}

6
src/plfa/part2/Confluence.lagda.md
View file

@ -221,7 +221,7 @@ The proof is by induction on `M ⇛ N`.
* Suppose `L · M ⇛ L′ · M′` because `L ⇛ L′` and `M ⇛ M′`. * Suppose `L · M ⇛ L′ · M′` because `L ⇛ L′` and `M ⇛ M′`.
By the induction hypothesis, we have `L —↠ L′` and `M —↠ M′`. By the induction hypothesis, we have `L —↠ L′` and `M —↠ M′`.
So `L · M —↠ L′ · M` and then `L′ · M —↠ L′ · M′` So `L · M —↠ L′ · M` and then `L′ · M —↠ L′ · M′`
because `—↠` is a congruence. because `—↠` is a congruence.
* Suppose `(ƛ N) · M ⇛ N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`. * Suppose `(ƛ N) · M ⇛ N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`.
By similar reasoning, we have By similar reasoning, we have
@ -451,7 +451,7 @@ par-triangle (papp {L = _ · _} p1 p2) = papp (par-triangle p1) (par-triangle p2
The proof of the triangle property is an induction on `M ⇛ N`. The proof of the triangle property is an induction on `M ⇛ N`.
* Suppose `x ⇛ x`. Clearly `x ⁺ = x`, so `x ⇛ x`. * Suppose `x ⇛ x`. Clearly `x ⁺ = x`, so `x ⇛ x`.
* Suppose `ƛ M ⇛ ƛ N`. By the induction hypothesis we have `N ⇛ M ⁺` * Suppose `ƛ M ⇛ ƛ N`. By the induction hypothesis we have `N ⇛ M ⁺`
and by definition `(λ M) ⁺ = λ (M ⁺)`, so we conclude that `λ N ⇛ λ and by definition `(λ M) ⁺ = λ (M ⁺)`, so we conclude that `λ N ⇛ λ
@ -619,7 +619,7 @@ and `par-confluence` are based on the notion of complete development
by Takahashi (1995) and Pfenning's 1992 technical report about the by Takahashi (1995) and Pfenning's 1992 technical report about the
Church-Rosser theorem. In addition, we consulted Nipkow and Church-Rosser theorem. In addition, we consulted Nipkow and
Berghofer's mechanization in Isabelle, which is based on an earlier Berghofer's mechanization in Isabelle, which is based on an earlier
article by Nipkow (JAR 1996). article by Nipkow (JAR 1996).
## Unicode ## Unicode

12
style-guide.md
View file

@ -2,7 +2,7 @@ Style guide for PLFA
============================ ============================
This is based on [the style guide for the Agda standard library](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md). This is based on [the style guide for the Agda standard library](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
Like it, this is very much a work-in-progress and is not exhaustive. Like it, this is very much a work-in-progress and is not exhaustive.
## File structure ## File structure
@ -44,14 +44,14 @@ Like it, this is very much a work-in-progress and is not exhaustive.
* If the type of a term does not fit on one line then the subsequent * If the type of a term does not fit on one line then the subsequent
lines of the type should all be indented by two spaces, e.g. lines of the type should all be indented by two spaces, e.g.
```agda ```agda
map-cong₂ : ∀ {a b} {A : Set a} {B : Set b} map-cong₂ : ∀ {a b} {A : Set a} {B : Set b}
→ ∀ {f g : A → B} {xs} → ∀ {f g : A → B} {xs}
→ All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs → All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
``` ```
* As can be seen in the example above, function arrows at line breaks * As can be seen in the example above, function arrows at line breaks
should always go at the beginning of the next line rather than the should always go at the beginning of the next line rather than the
end of the line. end of the line.
#### Module parameters #### Module parameters
@ -85,7 +85,7 @@ Like it, this is very much a work-in-progress and is not exhaustive.
```agda ```agda
+-comm : Commutative _+_ +-comm : Commutative _+_
+-comm zero n = sym (+-identityʳ n) +-comm zero n = sym (+-identityʳ n)
+-comm (suc m) n = +-comm (suc m) n =
begin begin
suc m + n suc m + n
≡⟨⟩ ≡⟨⟩

28
travis-build-cache.sh
View file

@ -10,24 +10,24 @@
# - Create JSON request. # - Create JSON request.
# #
body=$(cat .travis.yml \ body=$(cat .travis.yml \
| yq w - script "echo 'Done'"\ | yq w - script "echo 'Done'"\
| yq d - before_deploy \ | yq d - before_deploy \
| yq d - deploy \ | yq d - deploy \
| yq p - config \ | yq p - config \
| yq w - message "Build cache" \ | yq w - message "Build cache" \
| yq w - branch dev \ | yq w - branch dev \
| yq w - merge_mode replace \ | yq w - merge_mode replace \
| yq p - request -j) | yq p - request -j)
# Send request to Travis. # Send request to Travis.
# #
resp=$(curl -s -X POST \ resp=$(curl -s -X POST \
-H "Content-Type: application/json" \ -H "Content-Type: application/json" \
-H "Accept: application/json" \ -H "Accept: application/json" \
-H "Travis-API-Version: 3" \ -H "Travis-API-Version: 3" \
-H "Authorization: token $TRAVIS_TOKEN" \ -H "Authorization: token $TRAVIS_TOKEN" \
-d "$body" \ -d "$body" \
https://api.travis-ci.org/repo/plfa%2Fplfa.github.io/requests) https://api.travis-ci.org/repo/plfa%2Fplfa.github.io/requests)
# Output response. # Output response.
# #