From fc896bdc573a2c43116c8577a81fad43dd318119 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 24 Dec 2025 16:27:39 +0000 Subject: [PATCH 1/4] Add header shift to markdownToHtml5 --- tools/Buildfile.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tools/Buildfile.hs b/tools/Buildfile.hs index e96839cda..6a974e717 100644 --- a/tools/Buildfile.hs +++ b/tools/Buildfile.hs @@ -860,7 +860,11 @@ genericPostProcessHtml5 cmdOutput outDir out html = do -- | Convert Markdown to HTML5 using Pandoc. markdownToHtml5 :: (?getReferences :: () -> Action MetaValue) => Text -> Action Text -markdownToHtml5 = Pandoc.markdownToPandoc >=> processCitations >=> Pandoc.pandocToHtml5 +markdownToHtml5 = + Pandoc.markdownToPandoc + >=> pure . Pandoc.shiftHeadersBy 1 + >=> processCitations + >=> Pandoc.pandocToHtml5 -- | Process Markdown citations with citeproc using the references returned by @?getReferences@. processCitations :: (?getReferences :: () -> Action MetaValue) => Pandoc -> Action Pandoc From c53b1953c774efdcc934f5a4fdd0440d05892021 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 24 Dec 2025 15:00:30 +0000 Subject: [PATCH 2/4] Fix headers in main text --- src/plfa/part1/Connectives.lagda.md | 32 ++-- src/plfa/part1/Decidable.lagda.md | 30 ++-- src/plfa/part1/Equality.lagda.md | 30 ++-- src/plfa/part1/Induction.lagda.md | 56 +++---- src/plfa/part1/Isomorphism.lagda.md | 28 ++-- src/plfa/part1/Lists.lagda.md | 80 +++++----- src/plfa/part1/Naturals.lagda.md | 48 +++--- src/plfa/part1/Negation.lagda.md | 22 +-- src/plfa/part1/Quantifiers.lagda.md | 34 ++--- src/plfa/part1/Relations.lagda.md | 52 +++---- src/plfa/part2/BigStep.lagda.md | 20 +-- src/plfa/part2/Bisimulation.lagda.md | 22 +-- src/plfa/part2/Confluence.lagda.md | 24 +-- src/plfa/part2/DeBruijn.lagda.md | 52 +++---- src/plfa/part2/Inference.lagda.md | 46 +++--- src/plfa/part2/Lambda.lagda.md | 76 +++++----- src/plfa/part2/More.lagda.md | 138 +++++++++--------- src/plfa/part2/Properties.lagda.md | 54 +++---- src/plfa/part2/Substitution.lagda.md | 34 ++--- src/plfa/part2/Untyped.lagda.md | 60 ++++---- src/plfa/part3/Adequacy.lagda.md | 16 +- src/plfa/part3/Compositional.lagda.md | 16 +- src/plfa/part3/ContextualEquivalence.lagda.md | 8 +- src/plfa/part3/Denotational.lagda.md | 38 ++--- src/plfa/part3/Soundness.lagda.md | 32 ++-- 25 files changed, 524 insertions(+), 524 deletions(-) diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index 4cbdb074a..74e0d666b 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -24,7 +24,7 @@ principle known as _Propositions as Types_: * _implication_ is _function space_. -## Imports +# Imports ```agda import Relation.Binary.PropositionalEquality as Eq @@ -37,7 +37,7 @@ open plfa.part1.Isomorphism.≃-Reasoning ``` -## Conjunction is product +# Conjunction is product Given two propositions `A` and `B`, the conjunction `A × B` holds if both `A` holds and `B` holds. We formalise this idea by @@ -245,7 +245,7 @@ For example, the type `(ℕ × Bool) × Tri` is _not_ the same as `ℕ × instance `⟨ ⟨ 1 , true ⟩ , aa ⟩`, which is a member of the former, corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter. -#### Exercise `⇔≃×` (practice) +## Exercise `⇔≃×` (practice) Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff) is isomorphic to `(A → B) × (B → A)`. @@ -255,7 +255,7 @@ is isomorphic to `(A → B) × (B → A)`. ``` -## Truth is unit +# Truth is unit Truth `⊤` always holds. We formalise this idea by declaring the empty record type. @@ -376,7 +376,7 @@ Here we have used a chain of isomorphisms, analogous to that used for equality. -## Disjunction is sum +# Disjunction is sum Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds if either `A` holds or `B` holds. We formalise this idea by @@ -487,7 +487,7 @@ possible arguments of type `Bool ⊎ Tri`: Sum on types also shares a property with sum on numbers in that it is commutative and associative _up to isomorphism_. -#### Exercise `⊎-comm` (recommended) +## Exercise `⊎-comm` (recommended) Show sum is commutative up to isomorphism. @@ -495,7 +495,7 @@ Show sum is commutative up to isomorphism. -- Your code goes here ``` -#### Exercise `⊎-assoc` (practice) +## Exercise `⊎-assoc` (practice) Show sum is associative up to isomorphism. @@ -503,7 +503,7 @@ Show sum is associative up to isomorphism. -- Your code goes here ``` -## False is empty +# False is empty False `⊥` never holds. We formalise this idea by declaring a suitable inductive type: @@ -569,7 +569,7 @@ type `⊥`. For numbers, zero is the identity of addition. Correspondingly, empty is the identity of sums _up to isomorphism_. -#### Exercise `⊥-identityˡ` (recommended) +## Exercise `⊥-identityˡ` (recommended) Show empty is the left identity of sums up to isomorphism. @@ -577,7 +577,7 @@ Show empty is the left identity of sums up to isomorphism. -- Your code goes here ``` -#### Exercise `⊥-identityʳ` (practice) +## Exercise `⊥-identityʳ` (practice) Show empty is the right identity of sums up to isomorphism. @@ -585,7 +585,7 @@ Show empty is the right identity of sums up to isomorphism. -- Your code goes here ``` -## Implication is function {#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 @@ -749,7 +749,7 @@ is the same as the assertion that if `A` holds then `B` holds and if ``` -## Distribution +# Distribution Products distribute over sum, up to isomorphism. The code to validate this fact is similar in structure to our previous results: @@ -810,7 +810,7 @@ second only corresponds to an embedding, revealing a sense in which one of these laws is "more true" than the other. -#### Exercise `⊎-weak-×` (recommended) +## Exercise `⊎-weak-×` (recommended) Show that the following property holds: @@ -827,7 +827,7 @@ distributive law, and explain how it relates to the weak version. ``` -#### Exercise `⊎×-implies-×⊎` (practice) +## Exercise `⊎×-implies-×⊎` (practice) Show that a disjunct of conjuncts implies a conjunct of disjuncts: @@ -843,7 +843,7 @@ Does the converse hold? If so, prove; if not, give a counterexample. ``` -## Standard library +# Standard library Definitions similar to those in this chapter can be found in the standard library: @@ -867,7 +867,7 @@ standard library is less convenient, since it is parameterised with respect to an arbitrary notion of equivalence. -## Unicode +# Unicode This chapter uses the following unicode: diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index da17b0b96..9569b3bf8 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -16,7 +16,7 @@ but later discover that these are best avoided in favour of a new notion of _decidable_. -## Imports +# Imports ```agda import Relation.Binary.PropositionalEquality as Eq @@ -33,7 +33,7 @@ open import plfa.part1.Relations using (_<_; z Date: Wed, 24 Dec 2025 16:35:22 +0000 Subject: [PATCH 3/4] Fix headers in auxiliary text --- courses/TSPL/2019/Assignment1.lagda.md | 64 +++++++------- courses/TSPL/2019/Assignment2.lagda.md | 84 +++++++++--------- courses/TSPL/2019/Assignment3.lagda.md | 92 +++++++++---------- courses/TSPL/2019/Assignment4.lagda.md | 118 ++++++++++++------------- courses/TSPL/2019/Exam.lagda.md | 68 +++++++------- courses/TSPL/2019/tspl2019.md | 18 ++-- courses/TSPL/2022/Assignment1.lagda.md | 68 +++++++------- courses/TSPL/2022/Assignment2.lagda.md | 80 ++++++++--------- courses/TSPL/2022/Assignment3.lagda.md | 114 ++++++++++++------------ courses/TSPL/2022/Assignment4.lagda.md | 56 ++++++------ courses/TSPL/2022/Eval.lagda.md | 28 +++--- courses/TSPL/2022/Exam.lagda.md | 68 +++++++------- courses/TSPL/2022/tspl.md | 24 ++--- courses/TSPL/2023/Assignment1.lagda.md | 68 +++++++------- courses/TSPL/2023/Assignment2.lagda.md | 78 ++++++++-------- courses/TSPL/2023/Assignment3.lagda.md | 110 +++++++++++------------ courses/TSPL/2023/Assignment4.lagda.md | 106 +++++++++++----------- courses/TSPL/2023/Eval.lagda.md | 28 +++--- courses/TSPL/2023/Exam.lagda.md | 68 +++++++------- courses/TSPL/2023/tspl.md | 24 ++--- courses/TSPL/2024/Assignment1.lagda.md | 70 +++++++-------- courses/TSPL/2024/Assignment2.lagda.md | 80 ++++++++--------- courses/TSPL/2024/Assignment3.lagda.md | 112 +++++++++++------------ courses/TSPL/2024/Assignment4.lagda.md | 106 +++++++++++----------- courses/TSPL/2024/tspl.md | 26 +++--- web/Citing.md | 18 ++-- web/Notes.md | 32 +++---- web/StyleGuide.md | 30 +++---- web/TableOfContents.md | 26 +++--- 29 files changed, 932 insertions(+), 932 deletions(-) diff --git a/courses/TSPL/2019/Assignment1.lagda.md b/courses/TSPL/2019/Assignment1.lagda.md index 2b7d85e5e..858b0e1c9 100644 --- a/courses/TSPL/2019/Assignment1.lagda.md +++ b/courses/TSPL/2019/Assignment1.lagda.md @@ -7,9 +7,9 @@ permalink : /TSPL/2019/Assignment1/ module Assignment1 where ``` -## YOUR NAME AND EMAIL GOES HERE +# YOUR NAME AND EMAIL GOES HERE -## Introduction +# Introduction You must do _all_ the exercises labelled "(recommended)". @@ -28,7 +28,7 @@ Please ensure your files execute correctly under Agda! -## Good Scholarly Practice. +# Good Scholarly Practice. Please remember the University requirement as regards all assessed work. Details about this can be found at: @@ -43,7 +43,7 @@ yourself, or your group in the case of group practicals). -## Imports +# Imports ```agda import Relation.Binary.PropositionalEquality as Eq @@ -55,24 +55,24 @@ open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm; open import plfa.part1.Relations using (_<_; z @@ -33,7 +33,7 @@ Please ensure your files execute correctly under Agda! before and after code you add, to indicate your changes. -## Good Scholarly Practice. +# Good Scholarly Practice. Please remember the University requirement as regards all assessed work. Details about this can be found at: @@ -47,7 +47,7 @@ permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals). -## Imports +# Imports ```agda import Relation.Binary.PropositionalEquality as Eq @@ -60,7 +60,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no) ``` -## DeBruijn +# DeBruijn ```agda @@ -74,26 +74,26 @@ Remember to indent all code by two spaces. ``` -#### Exercise (`mul`) (recommended) +### Exercise (`mul`) (recommended) Write out the definition of a lambda term that multiplies two natural numbers, now adapted to the inherently typed DeBruijn representation. -#### Exercise `V¬—→` +### Exercise `V¬—→` Following the previous development, show values do not reduce, and its corollary, terms that reduce are not values. -#### Exercise `mul-eval` (recommended) +### Exercise `mul-eval` (recommended) Using the evaluator, confirm that two times two is four. -## More +# More ```agda module More where @@ -102,7 +102,7 @@ module More where Remember to indent all code by two spaces. -### Syntax +## Syntax ```agda @@ -123,7 +123,7 @@ Remember to indent all code by two spaces. infix 9 #_ ``` -### Types +## Types ```agda data Type : Set where @@ -137,7 +137,7 @@ Remember to indent all code by two spaces. `List : Type → Type ``` -### Contexts +## Contexts ```agda data Context : Set where @@ -145,7 +145,7 @@ Remember to indent all code by two spaces. _,_ : Context → Type → Context ``` -### Variables and the lookup judgment +## Variables and the lookup judgment ```agda data _∋_ : Context → Type → Set where @@ -160,7 +160,7 @@ Remember to indent all code by two spaces. → Γ , A ∋ B ``` -### Terms and the typing judgment +## Terms and the typing judgment ```agda data _⊢_ : Context → Type → Set where @@ -259,7 +259,7 @@ Remember to indent all code by two spaces. ``` -### Abbreviating de Bruijn indices +## Abbreviating de Bruijn indices ```agda lookup : Context → ℕ → Type @@ -278,7 +278,7 @@ Remember to indent all code by two spaces. # n = ` count n ``` -## Renaming +# Renaming ```agda ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B) @@ -302,7 +302,7 @@ Remember to indent all code by two spaces. rename ρ (case× L M) = case× (rename ρ L) (rename (ext (ext ρ)) M) ``` -## Simultaneous Substitution +# Simultaneous Substitution ```agda exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B) @@ -326,7 +326,7 @@ Remember to indent all code by two spaces. subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M) ``` -## Single and double substitution +# Single and double substitution ```agda _[_] : ∀ {Γ A B} @@ -354,7 +354,7 @@ Remember to indent all code by two spaces. σ (S (S x)) = ` x ``` -## Values +# Values ```agda data Value : ∀ {Γ A} → Γ ⊢ A → Set where @@ -394,7 +394,7 @@ Remember to indent all code by two spaces. Implicit arguments need to be supplied when they are not fixed by the given arguments. -## Reduction +# Reduction ```agda infix 2 _—→_ @@ -524,7 +524,7 @@ not fixed by the given arguments. → case× ⟨ V , W ⟩ M —→ M [ V ][ W ] ``` -## Reflexive and transitive closure +# Reflexive and transitive closure ```agda infix 2 _—↠_ @@ -552,7 +552,7 @@ not fixed by the given arguments. ``` -## Values do not reduce +# Values do not reduce ```agda V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A} @@ -568,7 +568,7 @@ not fixed by the given arguments. ``` -## Progress +# Progress ```agda data Progress {A} (M : ∅ ⊢ A) : Set where @@ -629,7 +629,7 @@ not fixed by the given arguments. ``` -## Evaluation +# Evaluation ```agda record Gas : Set where @@ -668,7 +668,7 @@ not fixed by the given arguments. ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` -## Examples +# Examples ```agda cube : ∅ ⊢ Nat ⇒ Nat @@ -744,7 +744,7 @@ not fixed by the given arguments. ``` -#### Exercise `More` (recommended in part) +### Exercise `More` (recommended in part) Formalise the remaining constructs defined in this chapter. Evaluate each example, applied to data as needed, @@ -757,16 +757,16 @@ to confirm it returns the expected answer. * lists -## Bisimulation +# Bisimulation (No recommended exercises for this chapter.) -#### Exercise `sim⁻¹` +### Exercise `sim⁻¹` Show that we also have a simulation in the other direction, and hence that we have a bisimulation. -#### Exercise `products` +### Exercise `products` Show that the two formulations of products in Chapter [More][plfa.More] @@ -774,7 +774,7 @@ are in bisimulation. The only constructs you need to include are variables, and those connected to functions and products. In this case, the simulation is _not_ lock-step. -## Inference +# Inference ```agda module Inference where @@ -782,13 +782,13 @@ module Inference where Remember to indent all code by two spaces. -### Imports +## Imports ```agda import plfa.part2.More as DB ``` -### Syntax +## Syntax ```agda infix 4 _∋_⦂_ @@ -806,7 +806,7 @@ Remember to indent all code by two spaces. infix 9 `_ ``` -### Identifiers, types, and contexts +## Identifiers, types, and contexts ```agda Id : Set @@ -821,7 +821,7 @@ Remember to indent all code by two spaces. _,_⦂_ : Context → Id → Type → Context ``` -### Terms +## Terms ```agda data Term⁺ : Set @@ -841,7 +841,7 @@ Remember to indent all code by two spaces. _↑ : Term⁺ → Term⁻ ``` -### Sample terms +## Sample terms ```agda two : Term⁻ @@ -854,7 +854,7 @@ Remember to indent all code by two spaces. ↓ `ℕ ⇒ `ℕ ⇒ `ℕ ``` -### Lookup +## Lookup ```agda data _∋_⦂_ : Context → Id → Type → Set where @@ -870,7 +870,7 @@ Remember to indent all code by two spaces. → Γ , y ⦂ B ∋ x ⦂ A ``` -### Bidirectional type checking +## Bidirectional type checking ```agda data _⊢_↑_ : Context → Term⁺ → Type → Set @@ -930,7 +930,7 @@ Remember to indent all code by two spaces. ``` -### Type equality +## Type equality ```agda _≟Tp_ : (A B : Type) → Dec (A ≡ B) @@ -944,7 +944,7 @@ Remember to indent all code by two spaces. ... | yes refl | yes refl = yes refl ``` -### Prerequisites +## Prerequisites ```agda dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′ @@ -958,7 +958,7 @@ Remember to indent all code by two spaces. ``` -### Unique lookup +## Unique lookup ```agda uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B @@ -968,7 +968,7 @@ Remember to indent all code by two spaces. uniq-∋ (S _ ∋x) (S _ ∋x′) = uniq-∋ ∋x ∋x′ ``` -### Unique synthesis +## Unique synthesis ```agda uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B @@ -977,7 +977,7 @@ Remember to indent all code by two spaces. uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl ``` -## Lookup type of a variable in the context +# Lookup type of a variable in the context ```agda ext∋ : ∀ {Γ B x y} @@ -999,7 +999,7 @@ Remember to indent all code by two spaces. ... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩ ``` -### Promoting negations +## Promoting negations ```agda ¬arg : ∀ {Γ A B L M} @@ -1018,7 +1018,7 @@ Remember to indent all code by two spaces. ``` -## Synthesize and inherit types +# Synthesize and inherit types ```agda synthesize : ∀ (Γ : Context) (M : Term⁺) @@ -1070,7 +1070,7 @@ Remember to indent all code by two spaces. ... | yes A≡B = yes (⊢↑ ⊢M A≡B) ``` -### Erasure +## Erasure ```agda ∥_∥Tp : Type → DB.Type @@ -1100,25 +1100,25 @@ Remember to indent all code by two spaces. ∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺ ``` -#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul} +### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul} Rewrite your definition of multiplication from Chapter [Lambda][plfa.Lambda], decorated to support inference. -#### Exercise `bidirectional-products` (recommended) {#bidirectional-products} +### Exercise `bidirectional-products` (recommended) {#bidirectional-products} Extend the bidirectional type rules to include products from Chapter [More][plfa.More]. -#### Exercise `bidirectional-rest` (stretch) +### Exercise `bidirectional-rest` (stretch) Extend the bidirectional type rules to include the rest of the constructs from Chapter [More][plfa.More]. -#### Exercise `inference-mul` (recommended) +### Exercise `inference-mul` (recommended) Rewrite your definition of multiplication from Chapter [Lambda][plfa.Lambda] decorated to support inference, and show @@ -1126,53 +1126,53 @@ that erasure of the inferred typing yields your definition of multiplication from Chapter [DeBruijn][plfa.DeBruijn]. -#### Exercise `inference-products` (recommended) +### Exercise `inference-products` (recommended) Extend bidirectional inference to include products from Chapter [More][plfa.More]. -#### Exercise `inference-rest` (stretch) +### Exercise `inference-rest` (stretch) Extend bidirectional inference to include the rest of the constructs from Chapter [More][plfa.More]. -## Untyped +# Untyped -#### Exercise (`Type≃⊤`) +### Exercise (`Type≃⊤`) Show that `Type` is isomorphic to `⊤`, the unit type. -#### Exercise (`Context≃ℕ`) +### Exercise (`Context≃ℕ`) Show that `Context` is isomorphic to `ℕ`. -#### Exercise (`variant-1`) +### Exercise (`variant-1`) How would the rules change if we want call-by-value where terms normalise completely? Assume that `β` should not permit reduction unless both terms are in normal form. -#### Exercise (`variant-2`) +### Exercise (`variant-2`) How would the rules change if we want call-by-value where terms do not reduce underneath lambda? Assume that `β` permits reduction when both terms are values (that is, lambda abstractions). What would `plusᶜ · twoᶜ · twoᶜ` reduce to in this case? -#### Exercise `plus-eval` +### Exercise `plus-eval` Use the evaluator to confirm that `plus · two · two` and `four` normalise to the same term. -#### Exercise `multiplication-untyped` (recommended) +### Exercise `multiplication-untyped` (recommended) Use the encodings above to translate your definition of multiplication from previous chapters with the Scott representation and the encoding of the fixpoint operator. Confirm that two times two is four. -#### Exercise `encode-more` (stretch) +### Exercise `encode-more` (stretch) Along the lines above, encode all of the constructs of Chapter [More][plfa.More], diff --git a/courses/TSPL/2019/Exam.lagda.md b/courses/TSPL/2019/Exam.lagda.md index d5151bb7c..ea273a0ba 100644 --- a/courses/TSPL/2019/Exam.lagda.md +++ b/courses/TSPL/2019/Exam.lagda.md @@ -15,7 +15,7 @@ module Exam where before and after code you add, to indicate your changes. -## Imports +# Imports ```agda import Relation.Binary.PropositionalEquality as Eq @@ -29,7 +29,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Binary using (Decidable) ``` -## Problem 1 +# Problem 1 ```agda module Problem1 where @@ -39,12 +39,12 @@ module Problem1 where Remember to indent all code by two spaces. -### (a) +## (a) -### (b) +## (b) -## Problem 2 +# Problem 2 Remember to indent all code by two spaces. @@ -52,7 +52,7 @@ Remember to indent all code by two spaces. module Problem2 where ``` -### Infix declarations +## Infix declarations ```agda infix 4 _⊢_ @@ -70,7 +70,7 @@ module Problem2 where infix 9 #_ ``` -### Types and contexts +## Types and contexts ```agda data Type : Set where @@ -82,7 +82,7 @@ module Problem2 where _,_ : Context → Type → Context ``` -### Variables and the lookup judgment +## Variables and the lookup judgment ```agda data _∋_ : Context → Type → Set where @@ -97,7 +97,7 @@ module Problem2 where → Γ , B ∋ A ``` -### Terms and the typing judgment +## Terms and the typing judgment ```agda data _⊢_ : Context → Type → Set where @@ -140,7 +140,7 @@ module Problem2 where → Γ ⊢ A ``` -### Abbreviating de Bruijn indices +## Abbreviating de Bruijn indices ```agda lookup : Context → ℕ → Type @@ -159,7 +159,7 @@ module Problem2 where # n = ` count n ``` -### Renaming +## Renaming ```agda ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) @@ -181,7 +181,7 @@ module Problem2 where rename ρ (μ N) = μ (rename (ext ρ) N) ``` -### Simultaneous Substitution +## Simultaneous Substitution ```agda exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) @@ -203,7 +203,7 @@ module Problem2 where subst σ (μ N) = μ (subst (exts σ) N) ``` -### Single substitution +## Single substitution ```agda _[_] : ∀ {Γ A B} @@ -218,7 +218,7 @@ module Problem2 where σ (S x) = ` x ``` -### Values +## Values ```agda data Value : ∀ {Γ A} → Γ ⊢ A → Set where @@ -237,7 +237,7 @@ module Problem2 where → Value (`suc V) ``` -### Reduction +## Reduction ```agda infix 2 _—→_ @@ -285,7 +285,7 @@ module Problem2 where ``` -### Reflexive and transitive closure +## Reflexive and transitive closure ```agda infix 2 _—↠_ @@ -313,7 +313,7 @@ module Problem2 where ``` -### Progress +## Progress ```agda data Progress {A} (M : ∅ ⊢ A) : Set where @@ -347,7 +347,7 @@ module Problem2 where progress (μ N) = step (β-μ) ``` -### Evaluation +## Evaluation ```agda record Gas : Set where @@ -386,7 +386,7 @@ module Problem2 where ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` -## Problem 3 +# Problem 3 Remember to indent all code by two spaces. @@ -394,13 +394,13 @@ Remember to indent all code by two spaces. module Problem3 where ``` -### Imports +## Imports ```agda import plfa.part2.DeBruijn as DB ``` -### Syntax +## Syntax ```agda infix 4 _∋_⦂_ @@ -417,7 +417,7 @@ module Problem3 where infix 9 `_ ``` -### Types +## Types ```agda data Type : Set where @@ -425,14 +425,14 @@ module Problem3 where `ℕ : Type ``` -### Identifiers +## Identifiers ```agda Id : Set Id = String ``` -### Contexts +## Contexts ```agda data Context : Set where @@ -440,7 +440,7 @@ module Problem3 where _,_⦂_ : Context → Id → Type → Context ``` -### Terms +## Terms ```agda data Term⁺ : Set @@ -460,7 +460,7 @@ module Problem3 where _↑ : Term⁺ → Term⁻ ``` -### Lookup +## Lookup ```agda data _∋_⦂_ : Context → Id → Type → Set where @@ -476,7 +476,7 @@ module Problem3 where → Γ , y ⦂ B ∋ x ⦂ A ``` -### Bidirectional type checking +## Bidirectional type checking ```agda data _⊢_↑_ : Context → Term⁺ → Type → Set @@ -536,7 +536,7 @@ module Problem3 where ``` -### Type equality +## Type equality ```agda _≟Tp_ : (A B : Type) → Dec (A ≡ B) @@ -550,7 +550,7 @@ module Problem3 where ... | yes refl | yes refl = yes refl ``` -### Prerequisites +## Prerequisites ```agda dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′ @@ -564,7 +564,7 @@ module Problem3 where ``` -### Unique lookup +## Unique lookup ```agda uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B @@ -574,7 +574,7 @@ module Problem3 where uniq-∋ (S _ ∋x) (S _ ∋x′) = uniq-∋ ∋x ∋x′ ``` -### Unique synthesis +## Unique synthesis ```agda uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B @@ -583,7 +583,7 @@ module Problem3 where uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl ``` -## Lookup type of a variable in the context +# Lookup type of a variable in the context ```agda ext∋ : ∀ {Γ B x y} @@ -606,7 +606,7 @@ module Problem3 where ... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩ ``` -### Promoting negations +## Promoting negations ```agda ¬arg : ∀ {Γ A B L M} @@ -625,7 +625,7 @@ module Problem3 where ``` -## Synthesize and inherit types +# Synthesize and inherit types ```agda synthesize : ∀ (Γ : Context) (M : Term⁺) diff --git a/courses/TSPL/2019/tspl2019.md b/courses/TSPL/2019/tspl2019.md index a8b61da93..bebf4f199 100644 --- a/courses/TSPL/2019/tspl2019.md +++ b/courses/TSPL/2019/tspl2019.md @@ -3,7 +3,7 @@ title : "TSPL: Course notes" permalink : /TSPL/2019/ --- -## Staff +# Staff * **Instructor** [Philip Wadler](https://homepages.inf.ed.ac.uk/wadler) @@ -11,7 +11,7 @@ permalink : /TSPL/2019/ - [Wen Kokke](mailto:wen.kokke@ed.ac.uk) - [Orestis Melkonian](mailto:o.melkonian@sms.ed.ac.uk) -## Lectures +# Lectures Lectures take place Monday, Wednesday, and Friday in AT 5.07. * **10.00--10.50am** Lecture @@ -99,7 +99,7 @@ Lectures take place Monday, Wednesday, and Friday in AT 5.07. -## Assessment +# Assessment Assessment for the course is as follows. @@ -118,7 +118,7 @@ the optional project may not be a good use of time compared to other courses where there are easier marks to be had. -## Coursework +# Coursework For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/). @@ -140,7 +140,7 @@ submit tspl cwN AssignmentN.lagda.md where N is the number of the assignment. -## Optional project +# Optional project The optional project is to take a research paper and formalise all or part of it in Agda. I suggest formalising the paper @@ -156,14 +156,14 @@ Submit the optional project by running submit tspl essay Essay.lagda.md ``` -## Mock exam +# Mock exam 10am-12noon Friday 29 November, AT 5.05 West Lab. An online examination with the Agda proof assistant, under DICE to let you practice for the exam and familiarise yourself with exam conditions. -## Additional reading +# Additional reading * John Reynolds, [Three Approaches to Type Structure][reynolds], @@ -186,7 +186,7 @@ practice for the exam and familiarise yourself with exam conditions. -## Optional project +# Optional project The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional @@ -180,14 +180,14 @@ submit tspl essay Essay.lagda.md --> -## Mock exam +# Mock exam 10am-12noon Monday 28 November. An online examination with the Agda proof assistant, to let you practice for the exam and familiarise yourself with exam conditions. -## Additional reading +# Additional reading * John Reynolds, [Three Approaches to Type Structure][reynolds], @@ -208,7 +208,7 @@ practice for the exam and familiarise yourself with exam conditions. -## Optional project +# Optional project The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional @@ -188,14 +188,14 @@ submit tspl essay Essay.lagda.md --> -## Additional reading +# Additional reading * John Reynolds, [Three Approaches to Type Structure][reynolds], @@ -220,7 +220,7 @@ practice for the exam and familiarise yourself with exam conditions. [p-as-t]: https://dl.acm.org/doi/10.1145/2699407 -## Essay +# Essay The essay is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb @@ -177,14 +177,14 @@ essays that contributed to ongoing research. Talk to Prof Wadler about what you would like to submit. -## Additional reading +# Additional reading * John Reynolds, [Three Approaches to Type Structure][reynolds], @@ -209,7 +209,7 @@ practice for the exam and familiarise yourself with exam conditions. [p-as-t]: https://dl.acm.org/doi/10.1145/2699407 -### Courses taught from the textbook +## Courses taught from the textbook -#### 2025 +### 2025 * [Peter Thiemann, Albert-Ludwigs University][Freiburg-2025] * [Joseph Eremondi, University of Regina][EremondiPage] [Freiburg-2025]: https://proglang.github.io/teaching/25ss/eopl.html [EremondiPage]: https://www2.cs.uregina.ca/~eremondj/ -#### 2024 +### 2024 * [Philip Wadler, University of Edinburgh][TSPL-2024] [TSPL-2024]: /TSPL/2024/ -#### 2023 +### 2023 * [Peter Thiemann, Albert-Ludwigs University][Freiburg-2023] * [Philip Wadler, University of Edinburgh][TSPL-2023] [Freiburg-2023]: https://web.archive.org/web/20240208112146/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2023ws/ [TSPL-2023]: /TSPL/2023/ -#### 2022 +### 2022 * [Andrej Bauer, University of Ljubljana][UL-2022] * Michael Shulman, University of San Diego @@ -72,7 +72,7 @@ $endfor$ [Freiburg-2022]: https://web.archive.org/web/20220810154516/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2022ss/ [TSPL-2022]: /TSPL/2022/ -#### 2021 +### 2021 * Favonia, University of Minnesota * [Prabhakar Ragde, University of Waterloo][UW-2021] @@ -81,7 +81,7 @@ $endfor$ [UW-2021]: https://web.archive.org/web/20210424214202/https://cs.uwaterloo.ca/~plragde/747/ [McM-2021]: https://github.com/JacquesCarette/CAS706-F2021/ -#### 2020 +### 2020 * [William Cook, University of Texas][UT-2020] * [Maria Emilia Maietti and Ingo Blechschmidt, Università di Padova][Padova-2020] * [John Maraist, University of Wisconsin-La Crosse][UWL-2020] @@ -94,7 +94,7 @@ $endfor$ [UWL-2020]: https://web.archive.org/web/20220810155032/https://github.com/jphmrst/PLC/tree/fall2020#readme [IU-2020]: https://web.archive.org/web/20220421134334/https://jsiek.github.io/B522-PL-Foundations/ -#### 2019 +### 2019 * [Dan Ghica, University of Birmingham][BHAM-2019] * [Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup][SFPL-Meetup-2019] * [Prabhakar Ragde, University of Waterloo][UW-2019] @@ -110,7 +110,7 @@ $endfor$ [EUSA-2020]: https://web.archive.org/web/20201130051416/https://www.eusa.ed.ac.uk/representation/campaigns/teachingawards2020/ -#### 2018 +### 2018 * [David Darais, University of Vermont][UVM-2018] * [Philip Wadler, University of Edinburgh][TSPL-2018] * John Leo, Google Seattle @@ -119,7 +119,7 @@ $endfor$ [TSPL-2018]: https://plfa.github.io/19.08/TSPL/2018/ [UVM-2018]: https://web.archive.org/web/20190324115921/https://david.darais.com/courses/fa2018-cs295A/ -### Derived works +## Derived works * [PLFArend](https://github.com/marat-rkh/PLFArend): the PLFA book with all code snippets rewritten in Arend. * [PLFaLean](https://github.com/rami3l/PLFaLean): PLFA proofs implemented in Lean 4, covering Parts 2-3 of the v22.08 release of the book. From 5a60929dbbe37aeb729dc1e614a99fd37c019144 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 24 Dec 2025 16:51:51 +0000 Subject: [PATCH 4/4] Enable markdownlint test for header increments --- .markdownlint.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.markdownlint.yaml b/.markdownlint.yaml index 2b2218b1f..4426414b0 100644 --- a/.markdownlint.yaml +++ b/.markdownlint.yaml @@ -1,11 +1,11 @@ default: true -MD001: false MD004: false MD007: false MD012: false MD013: false MD022: false MD024: false +MD025: false MD030: false MD032: false MD033: false