Fixed syntax for assigning anchors.
This commit is contained in:
Wen Kokke
parent
4b5d775ba1
commit
07d082c9db
17 changed files with 54 additions and 53 deletions
|
|
@ -23,7 +23,7 @@ $(SITE_DIR)/plfa.epub: \
|
|||
$(RAW_DIR)/epub.md $(EPUB_DIR)/epub.css $(RAW_DIR)/epub.xml $(FRANKENFONT) \
|
||||
$(MD_FILES) $(EPUB_LUA_SCRIPTS) | setup-install-pandoc
|
||||
@echo "Building EPUB"
|
||||
$(PANDOC) \
|
||||
@$(PANDOC) \
|
||||
--strip-comments \
|
||||
--css=$(EPUB_DIR)/epub.css \
|
||||
--epub-embed-font=$(FRANKENFONT) \
|
||||
|
|
@ -33,6 +33,7 @@ $(SITE_DIR)/plfa.epub: \
|
|||
--lua-filter=$(EPUB_LUA_DIR)/remove-badges.lua -M badge-url=https://img.shields.io/badge/ \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/epub-clean-html.lua \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/single-file-links.lua \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/single-file-identifiers.lua \
|
||||
--standalone \
|
||||
--toc --toc-depth=2 \
|
||||
--epub-chapter-level=2 \
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
-- [text](/chapter/) -> [text](#chapter)
|
||||
--
|
||||
-- All other Links are ignored.
|
||||
function Link (el)
|
||||
function Link(el)
|
||||
local n
|
||||
-- Case 1:
|
||||
el.target, n = el.target:gsub("^/(%w+)/#([%w-]+)$", "#%1-%2")
|
||||
|
|
|
|||
|
|
@ -4,6 +4,6 @@ title: "PLFA as EPUB"
|
|||
|
||||
It has been just over a year and a half since this feature was first requested in [#112][issue112]… Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][EPUB]
|
||||
|
||||
[EPUB]: https://plfa.github.io/out/epub/plfa.epub
|
||||
[EPUB]: https://plfa.github.io/epub/plfa.epub
|
||||
[issue112]: https://github.com/plfa/plfa.github.io/issues/112
|
||||
[mreed20]: https://github.com/mreed20
|
||||
|
|
|
|||
|
|
@ -21,8 +21,8 @@ As always, bug reports and pull requests are very, very welcome!
|
|||
[Altariarite]: https://github.com/Altariarite
|
||||
[mreed20]: https://github.com/mreed20
|
||||
|
||||
[PDF]: https://plfa.github.io/out/epub/plfa.pdf
|
||||
[EPUB]: https://plfa.github.io/out/epub/plfa.epub
|
||||
[PDF]: https://plfa.github.io/epub/plfa.pdf
|
||||
[EPUB]: https://plfa.github.io/epub/plfa.epub
|
||||
|
||||
[issue577]: https://github.com/plfa/plfa.github.io/issues/577
|
||||
[issue578]: https://github.com/plfa/plfa.github.io/issues/578
|
||||
|
|
|
|||
|
|
@ -536,7 +536,7 @@ Show empty is the right identity of sums up to isomorphism.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
## Implication is function {name=implication}
|
||||
## Implication is function {#implication}
|
||||
|
||||
Given two propositions `A` and `B`, the implication `A → B` holds if
|
||||
whenever `A` holds then `B` must also hold. We formalise implication using
|
||||
|
|
|
|||
|
|
@ -561,7 +561,7 @@ postulate
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
## Proof by reflection {name=proof-by-reflection}
|
||||
## Proof by reflection {#proof-by-reflection}
|
||||
|
||||
Let's revisit our definition of monus from
|
||||
Chapter [Naturals](/Naturals/).
|
||||
|
|
|
|||
|
|
@ -132,7 +132,7 @@ Again, a useful exercise is to carry out an interactive development,
|
|||
checking how Agda's knowledge changes as each of the two arguments is
|
||||
instantiated.
|
||||
|
||||
## Congruence and substitution {name=cong}
|
||||
## Congruence and substitution {#cong}
|
||||
|
||||
Equality satisfies _congruence_. If two terms are equal,
|
||||
they remain so after the same function is applied to both:
|
||||
|
|
@ -635,7 +635,7 @@ Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
|
|||
draft, 2017.)
|
||||
|
||||
|
||||
## Universe polymorphism {name=unipoly}
|
||||
## Universe polymorphism {#unipoly}
|
||||
|
||||
As we have seen, not every type belongs to `Set`, but instead every
|
||||
type belongs somewhere in the hierarchy `Set₀`, `Set₁`, `Set₂`, and so on,
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ distributes over another operator. A careful author will often call
|
|||
out these properties---or their lack---for instance by pointing out
|
||||
that a newly introduced operator is associative but not commutative.
|
||||
|
||||
#### Exercise `operators` (practice) {name=operators}
|
||||
#### Exercise `operators` (practice) {#operators}
|
||||
|
||||
Give another example of a pair of operators that have an identity
|
||||
and are associative, commutative, and distribute over one another.
|
||||
|
|
@ -599,7 +599,7 @@ the main proposition first, and the equations required to do so
|
|||
will suggest what lemmas to prove.
|
||||
|
||||
|
||||
## Our first corollary: rearranging {name=sections}
|
||||
## Our first corollary: rearranging {#sections}
|
||||
|
||||
We can apply associativity to rearrange parentheses however we like.
|
||||
Here is an example:
|
||||
|
|
@ -695,7 +695,7 @@ judgments where the first number is less than _m_.
|
|||
There is also a completely finite approach to generating the same equations,
|
||||
which is left as an exercise for the reader.
|
||||
|
||||
#### Exercise `finite-|-assoc` (stretch) {name=finite-plus-assoc}
|
||||
#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the
|
||||
first four days using a finite story of creation, as
|
||||
|
|
@ -857,7 +857,7 @@ typing `C-c C-r` will fill it in, completing the proof:
|
|||
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl
|
||||
|
||||
|
||||
#### Exercise `+-swap` (recommended) {name=plus-swap}
|
||||
#### Exercise `+-swap` (recommended) {#plus-swap}
|
||||
|
||||
Show
|
||||
|
||||
|
|
@ -872,7 +872,7 @@ is associative and commutative.
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {name=times-distrib-plus}
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
|
|
@ -885,7 +885,7 @@ for all naturals `m`, `n`, and `p`.
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {name=times-assoc}
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
|
|
@ -898,7 +898,7 @@ for all naturals `m`, `n`, and `p`.
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `*-comm` (practice) {name=times-comm}
|
||||
#### Exercise `*-comm` (practice) {#times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
|
|
@ -912,7 +912,7 @@ you will need to formulate and prove suitable lemmas.
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `0∸n≡0` (practice) {name=zero-monus}
|
||||
#### Exercise `0∸n≡0` (practice) {#zero-monus}
|
||||
|
||||
Show
|
||||
|
||||
|
|
@ -925,7 +925,7 @@ for all naturals `n`. Did your proof require induction?
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `∸-|-assoc` (practice) {name=monus-plus-assoc}
|
||||
#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
|
|
@ -949,7 +949,7 @@ Show the following three laws
|
|||
for all `m`, `n`, and `p`.
|
||||
|
||||
|
||||
#### Exercise `Bin-laws` (stretch) {name=Bin-laws}
|
||||
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin](/Naturals/#Bin)
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ g ∘′ f = λ x → g (f x)
|
|||
```
|
||||
|
||||
|
||||
## Extensionality {name=extensionality}
|
||||
## Extensionality {#extensionality}
|
||||
|
||||
Extensionality asserts that the only way to distinguish functions is
|
||||
by applying them; if two functions applied to the same argument always
|
||||
|
|
@ -450,7 +450,7 @@ postulate
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `_⇔_` (practice) {name=iff}
|
||||
#### Exercise `_⇔_` (practice) {#iff}
|
||||
|
||||
Define equivalence of propositions (also known as "if and only if") as follows:
|
||||
```
|
||||
|
|
@ -465,7 +465,7 @@ Show that equivalence is reflexive, symmetric, and transitive.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `Bin-embedding` (stretch) {name=Bin-embedding}
|
||||
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin](/Naturals/#Bin) and
|
||||
|
|
|
|||
|
|
@ -458,7 +458,7 @@ _ =
|
|||
```
|
||||
Now the time to reverse a list is linear in the length of the list.
|
||||
|
||||
## Map {name=Map}
|
||||
## Map {#Map}
|
||||
|
||||
Map applies a function to every element of a list to generate a corresponding list.
|
||||
Map is an example of a _higher-order function_, one which takes a function as an
|
||||
|
|
@ -558,7 +558,7 @@ Define a suitable map operator over trees:
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
## Fold {name=Fold}
|
||||
## Fold {#Fold}
|
||||
|
||||
Fold takes an operator and a value, and uses the operator to combine
|
||||
each of the elements of the list, taking the given value as the result
|
||||
|
|
@ -833,7 +833,7 @@ Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and
|
|||
```
|
||||
|
||||
|
||||
## All {name=All}
|
||||
## All {#All}
|
||||
|
||||
We can also define predicates over lists. Two of the most important
|
||||
are `All` and `Any`.
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ after zero; and `2` is shorthand for `suc (suc zero)`, which is the
|
|||
same as `suc 1`, the successor of one; and `3` is shorthand for the
|
||||
successor of two; and so on.
|
||||
|
||||
#### Exercise `seven` (practice) {name=seven}
|
||||
#### Exercise `seven` (practice) {#seven}
|
||||
|
||||
Write out `7` in longhand.
|
||||
|
||||
|
|
@ -287,7 +287,7 @@ Parentheses and semicolons are among the few characters that cannot
|
|||
appear in names, so we do not need extra spaces in the `using` list.
|
||||
|
||||
|
||||
## Operations on naturals are recursive functions {name=plus}
|
||||
## Operations on naturals are recursive functions {#plus}
|
||||
|
||||
Now that we have the natural numbers, what can we do with them?
|
||||
For instance, can we define arithmetic operations such as
|
||||
|
|
@ -425,7 +425,7 @@ is not like testimony in a court which must be weighed to determine
|
|||
whether the witness is trustworthy. Rather, it is ironclad. The
|
||||
other word for evidence, which we will use interchangeably, is _proof_.
|
||||
|
||||
#### Exercise `+-example` (practice) {name=plus-example}
|
||||
#### Exercise `+-example` (practice) {#plus-example}
|
||||
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`.
|
||||
|
||||
|
|
@ -486,7 +486,7 @@ Here we have omitted the signature declaring `_ : 2 * 3 ≡ 6`, since
|
|||
it can easily be inferred from the corresponding term.
|
||||
|
||||
|
||||
#### Exercise `*-example` (practice) {name=times-example}
|
||||
#### Exercise `*-example` (practice) {#times-example}
|
||||
|
||||
Compute `3 * 4`, writing out your reasoning as a chain of equations, using the equations for `*`.
|
||||
(You do not need to step through the evaluation of `+`.)
|
||||
|
|
@ -496,7 +496,7 @@ Compute `3 * 4`, writing out your reasoning as a chain of equations, using the e
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `_^_` (recommended) {name=power}
|
||||
#### Exercise `_^_` (recommended) {#power}
|
||||
|
||||
Define exponentiation, which is given by the following equations:
|
||||
|
||||
|
|
@ -566,7 +566,7 @@ _ =
|
|||
∎
|
||||
```
|
||||
|
||||
#### Exercise `∸-example₁` and `∸-example₂` (recommended) {name=monus-examples}
|
||||
#### Exercise `∸-example₁` and `∸-example₂` (recommended) {#monus-examples}
|
||||
|
||||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
|
@ -701,7 +701,7 @@ definitions is quite similar. They might be considered two sides of
|
|||
the same coin.
|
||||
|
||||
|
||||
## The story of creation, finitely {name=finite-creation}
|
||||
## The story of creation, finitely {#finite-creation}
|
||||
|
||||
The above story was told in a stratified way. First, we create
|
||||
the infinite set of naturals. We take that set as given when
|
||||
|
|
@ -872,7 +872,7 @@ Haskell requires time proportional to the sum of the logarithms of
|
|||
_m_ and _n_.
|
||||
|
||||
|
||||
#### Exercise `Bin` (stretch) {name=Bin}
|
||||
#### Exercise `Bin` (stretch) {#Bin}
|
||||
|
||||
A more efficient representation of natural numbers uses a binary
|
||||
rather than a unary system. We represent a number as a bitstring:
|
||||
|
|
|
|||
|
|
@ -438,7 +438,7 @@ postulate
|
|||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `Bin-isomorphism` (stretch) {name=Bin-isomorphism}
|
||||
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin](/Naturals/#Bin),
|
||||
|
|
|
|||
|
|
@ -241,7 +241,7 @@ lack---for instance by saying that a newly introduced relation is a
|
|||
partial order but not a total order.
|
||||
|
||||
|
||||
#### Exercise `orderings` (practice) {name=orderings}
|
||||
#### Exercise `orderings` (practice) {#orderings}
|
||||
|
||||
Give an example of a preorder that is not a partial order.
|
||||
|
||||
|
|
@ -359,7 +359,7 @@ and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive
|
|||
hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal
|
||||
follows by congruence.
|
||||
|
||||
#### Exercise `≤-antisym-cases` (practice) {name=leq-antisym-cases}
|
||||
#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
|
||||
|
||||
The above proof omits cases where one argument is `z≤n` and one
|
||||
argument is `s≤s`. Why is it ok to omit them?
|
||||
|
|
@ -559,7 +559,7 @@ Show that multiplication is monotonic with regard to inequality.
|
|||
```
|
||||
|
||||
|
||||
## Strict inequality {name=strict-inequality}
|
||||
## Strict inequality {#strict-inequality}
|
||||
|
||||
We can define strict inequality similarly to inequality:
|
||||
```
|
||||
|
|
@ -597,7 +597,7 @@ and conversely. One can then give an alternative derivation of the
|
|||
properties of strict inequality, such as transitivity, by
|
||||
exploiting the corresponding properties of inequality.
|
||||
|
||||
#### Exercise `<-trans` (recommended) {name=less-trans}
|
||||
#### Exercise `<-trans` (recommended) {#less-trans}
|
||||
|
||||
Show that strict inequality is transitive.
|
||||
|
||||
|
|
@ -605,7 +605,7 @@ Show that strict inequality is transitive.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `trichotomy` (practice) {name=trichotomy}
|
||||
#### Exercise `trichotomy` (practice) {#trichotomy}
|
||||
|
||||
Show that strict inequality satisfies a weak version of trichotomy, in
|
||||
the sense that for any `m` and `n` that one of the following holds:
|
||||
|
|
@ -623,7 +623,7 @@ similar to that used for totality.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `+-mono-<` (practice) {name=plus-mono-less}
|
||||
#### Exercise `+-mono-<` (practice) {#plus-mono-less}
|
||||
|
||||
Show that addition is monotonic with respect to strict inequality.
|
||||
As with inequality, some additional definitions may be required.
|
||||
|
|
@ -632,7 +632,7 @@ As with inequality, some additional definitions may be required.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `≤-iff-<` (recommended) {name=leq-iff-less}
|
||||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||||
|
||||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||||
|
||||
|
|
@ -640,7 +640,7 @@ Show that `suc m ≤ n` implies `m < n`, and conversely.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `<-trans-revisited` (practice) {name=less-trans-revisited}
|
||||
#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
|
||||
|
||||
Give an alternative proof that strict inequality is transitive,
|
||||
using the relation between strict inequality and inequality and
|
||||
|
|
@ -749,7 +749,7 @@ evidence that the first number is odd. If it is because it is the
|
|||
successor of an even number, then the result is odd because it is the
|
||||
successor of the sum of two even numbers, which is even.
|
||||
|
||||
#### Exercise `o+o≡e` (stretch) {name=odd-plus-odd}
|
||||
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
|
||||
|
||||
Show that the sum of two odd numbers is even.
|
||||
|
||||
|
|
@ -757,7 +757,7 @@ Show that the sum of two odd numbers is even.
|
|||
-- Your code goes here
|
||||
```
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin](/Naturals/#Bin)
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ Chapter [Lambda](/Lambda/),
|
|||
and from it we compute an intrinsically-typed term, in the style of
|
||||
Chapter [DeBruijn](/DeBruijn/).
|
||||
|
||||
## Introduction: Inference rules as algorithms {name=algorithms}
|
||||
## Introduction: Inference rules as algorithms {#algorithms}
|
||||
|
||||
In the calculus we have considered so far, a term may have more than
|
||||
one type. For example,
|
||||
|
|
@ -470,7 +470,7 @@ the equality test in the application rule in the first
|
|||
[section](/Inference/#algorithms).
|
||||
|
||||
|
||||
#### Exercise `bidirectional-mul` (recommended) {name=bidirectional-mul}
|
||||
#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
|
||||
|
||||
Rewrite your definition of multiplication from
|
||||
Chapter [Lambda](/Lambda/), decorated to support inference.
|
||||
|
|
@ -480,7 +480,7 @@ Chapter [Lambda](/Lambda/), decorated to support inference.
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `bidirectional-products` (recommended) {name=bidirectional-products}
|
||||
#### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
|
||||
|
||||
Extend the bidirectional type rules to include products from
|
||||
Chapter [More](/More/).
|
||||
|
|
|
|||
|
|
@ -213,7 +213,7 @@ definition may use `plusᶜ` as defined earlier (or may not
|
|||
```
|
||||
|
||||
|
||||
#### Exercise `primed` (stretch) {name=primed}
|
||||
#### Exercise `primed` (stretch) {#primed}
|
||||
|
||||
Some people find it annoying to write `` ` "x" `` instead of `x`.
|
||||
We can make examples with lambda terms slightly easier to write
|
||||
|
|
@ -1201,7 +1201,7 @@ the three places where a bound variable is introduced.
|
|||
The rules are deterministic, in that at most one rule applies to every term.
|
||||
|
||||
|
||||
### Example type derivations {name=derivation}
|
||||
### Example type derivations {#derivation}
|
||||
|
||||
Type derivations correspond to trees. In informal notation, here
|
||||
is a type derivation for the Church numeral two,
|
||||
|
|
|
|||
|
|
@ -147,7 +147,7 @@ Here `M †` is the translation of term `M` from a calculus with the
|
|||
construct to a calculus without the construct.
|
||||
|
||||
|
||||
## Products {name=products}
|
||||
## Products {#products}
|
||||
|
||||
### Syntax
|
||||
|
||||
|
|
@ -285,7 +285,7 @@ We can also translate back the other way:
|
|||
(`proj₁ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ x ]
|
||||
(`proj₂ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ y ]
|
||||
|
||||
## Sums {name=sums}
|
||||
## Sums {#sums}
|
||||
|
||||
### Syntax
|
||||
|
||||
|
|
|
|||
|
|
@ -879,7 +879,7 @@ typed (C-suc c) = ⊢suc (typed c)
|
|||
typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs
|
||||
```
|
||||
|
||||
## Progress <a name="subtyping-progress"></a>
|
||||
## Progress <a #"subtyping-progress"></a>
|
||||
|
||||
The Progress theorem states that a well-typed term may either take a
|
||||
reduction step or it is already a value. The proof of Progress is like
|
||||
|
|
@ -952,7 +952,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
|
|||
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
|
||||
|
||||
|
||||
## Preservation <a name="subtyping-preservation"></a>
|
||||
## Preservation <a #"subtyping-preservation"></a>
|
||||
|
||||
In this section we prove that when a well-typed term takes a reduction
|
||||
step, the result is another well-typed term with the same type.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue