Skip to content

Commit 5c5fbe6

Browse files
authored
Ensure all code blocks are labeled and spaced (#1161)
1 parent f187ce7 commit 5c5fbe6

68 files changed

Lines changed: 2058 additions & 683 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.markdownlint.yaml

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
default: true
2+
MD001: false
3+
MD004: false
4+
MD007: false
5+
MD012: false
6+
MD013: false
7+
MD022: false
8+
MD024: false
9+
MD030: false
10+
MD032: false
11+
MD033: false
12+
MD038: false
13+
MD046: false
14+
MD049: false
15+
MD053: false
16+
MD059: false

.pre-commit-config.yaml

Lines changed: 23 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,28 @@
11
repos:
2-
- repo: https://github.com/pre-commit/pre-commit-hooks
2+
- repo: https://github.com/pre-commit/pre-commit-hooks
33
rev: v6.0.0
44
hooks:
5-
- id: check-added-large-files
6-
- id: check-case-conflict
7-
- id: check-executables-have-shebangs
8-
- id: check-json
9-
- id: check-merge-conflict
10-
- id: check-shebang-scripts-are-executable
11-
- id: check-symlinks
12-
- id: check-vcs-permalinks
13-
- id: check-yaml
14-
- id: destroyed-symlinks
15-
- id: detect-private-key
16-
- id: fix-byte-order-marker
17-
- id: file-contents-sorter
5+
- id: check-added-large-files
6+
- id: check-case-conflict
7+
- id: check-executables-have-shebangs
8+
- id: check-json
9+
- id: check-merge-conflict
10+
- id: check-shebang-scripts-are-executable
11+
- id: check-symlinks
12+
- id: check-vcs-permalinks
13+
- id: check-yaml
14+
- id: destroyed-symlinks
15+
- id: detect-private-key
16+
- id: fix-byte-order-marker
17+
- id: file-contents-sorter
1818
args: [--unique]
1919
files: '\.epubcheck\.tsv|\.htmlvalidateignore'
20-
- id: forbid-new-submodules
21-
- id: end-of-file-fixer
22-
- id: mixed-line-ending
23-
- id: trailing-whitespace
20+
- id: forbid-new-submodules
21+
- id: end-of-file-fixer
22+
- id: mixed-line-ending
23+
- id: trailing-whitespace
24+
- repo: https://github.com/igorshubovych/markdownlint-cli
25+
rev: v0.47.0
26+
hooks:
27+
- id: markdownlint
28+
files: 'src/.*\.md'

courses/TSPL/2019/Assignment1.lagda.md

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ title : "Assignment1: TSPL Assignment 1"
33
permalink : /TSPL/2019/Assignment1/
44
---
55

6-
```
6+
```agda
77
module Assignment1 where
88
```
99

@@ -19,9 +19,11 @@ You don't need to do all of these, but should attempt at least a few.
1919
Exercises labelled "(practice)" are included for those who want extra practice.
2020

2121
Submit your homework using the "submit" command.
22+
2223
```bash
2324
submit tspl cw1 Assignment1.lagda.md
2425
```
26+
2527
Please ensure your files execute correctly under Agda!
2628

2729

@@ -43,7 +45,7 @@ yourself, or your group in the case of group practicals).
4345

4446
## Imports
4547

46-
```
48+
```agda
4749
import Relation.Binary.PropositionalEquality as Eq
4850
open Eq using (_≡_; refl; cong; sym)
4951
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
@@ -89,12 +91,14 @@ Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equati
8991

9092
A more efficient representation of natural numbers uses a binary
9193
rather than a unary system. We represent a number as a bitstring.
92-
```
94+
95+
```agda
9396
data Bin : Set where
9497
nil : Bin
9598
x0_ : Bin → Bin
9699
x1_ : Bin → Bin
97100
```
101+
98102
For instance, the bitstring
99103

100104
1011

0 commit comments

Comments
 (0)