From 07d082c9db7dd05cf979abbc8833a0e2636af793 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 25 Aug 2021 00:17:03 +0100 Subject: [PATCH] Fixed syntax for assigning anchors. --- book/epub.mk | 3 ++- book/lua/single-file-links.lua | 2 +- posts/2020-06-02-plfa-as-epub.md | 2 +- posts/2021-08-24-plfa-as-pdf-and-epub.md | 4 ++-- src/plfa/part1/Connectives.lagda.md | 2 +- src/plfa/part1/Decidable.lagda.md | 2 +- src/plfa/part1/Equality.lagda.md | 4 ++-- src/plfa/part1/Induction.lagda.md | 20 ++++++++++---------- src/plfa/part1/Isomorphism.lagda.md | 6 +++--- src/plfa/part1/Lists.lagda.md | 6 +++--- src/plfa/part1/Naturals.lagda.md | 16 ++++++++-------- src/plfa/part1/Quantifiers.lagda.md | 2 +- src/plfa/part1/Relations.lagda.md | 20 ++++++++++---------- src/plfa/part2/Inference.lagda.md | 6 +++--- src/plfa/part2/Lambda.lagda.md | 4 ++-- src/plfa/part2/More.lagda.md | 4 ++-- src/plfa/part2/Subtyping.lagda.md | 4 ++-- 17 files changed, 54 insertions(+), 53 deletions(-) diff --git a/book/epub.mk b/book/epub.mk index 57946cc3..e25318f9 100644 --- a/book/epub.mk +++ b/book/epub.mk @@ -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 \ diff --git a/book/lua/single-file-links.lua b/book/lua/single-file-links.lua index 4d6498be..dcf5d61e 100644 --- a/book/lua/single-file-links.lua +++ b/book/lua/single-file-links.lua @@ -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") diff --git a/posts/2020-06-02-plfa-as-epub.md b/posts/2020-06-02-plfa-as-epub.md index 83f434c3..888e7c07 100644 --- a/posts/2020-06-02-plfa-as-epub.md +++ b/posts/2020-06-02-plfa-as-epub.md @@ -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 diff --git a/posts/2021-08-24-plfa-as-pdf-and-epub.md b/posts/2021-08-24-plfa-as-pdf-and-epub.md index c133ed7f..767387a7 100644 --- a/posts/2021-08-24-plfa-as-pdf-and-epub.md +++ b/posts/2021-08-24-plfa-as-pdf-and-epub.md @@ -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 diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index df116b15..34118dc1 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -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 diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index dc4a66b2..24a7b8e2 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -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/). diff --git a/src/plfa/part1/Equality.lagda.md b/src/plfa/part1/Equality.lagda.md index ec3cc5b1..8bd59d6d 100644 --- a/src/plfa/part1/Equality.lagda.md +++ b/src/plfa/part1/Equality.lagda.md @@ -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, diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index 7d19138f..37fc3448 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -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) diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index 2cee9aac..9b3f5334 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -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 diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 38d1e66e..8dcc3541 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -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`. diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 08931fb4..f6f1c199 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -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: diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index d44b71ff..66fb8c5c 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -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), diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 8d6f6bdb..34c12d82 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -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) diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index 75cd6099..d03e3cf9 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -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/). diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 31bd9b23..06472c8d 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -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, diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index 895be043..294ad94f 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -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 diff --git a/src/plfa/part2/Subtyping.lagda.md b/src/plfa/part2/Subtyping.lagda.md index 38de189f..71836424 100644 --- a/src/plfa/part2/Subtyping.lagda.md +++ b/src/plfa/part2/Subtyping.lagda.md @@ -879,7 +879,7 @@ typed (C-suc c) = ⊢suc (typed c) typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs ``` -## Progress +## Progress 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 +## Preservation 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.