Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions .markdownlint.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
default: true
MD001: false
MD004: false
MD007: false
MD012: false
MD013: false
MD022: false
MD024: false
MD030: false
MD032: false
MD033: false
MD038: false
MD046: false
MD049: false
MD053: false
MD059: false
41 changes: 23 additions & 18 deletions .pre-commit-config.yaml
Original file line number Diff line number Diff line change
@@ -1,23 +1,28 @@
repos:
- repo: https://github.com/pre-commit/pre-commit-hooks
- repo: https://github.com/pre-commit/pre-commit-hooks
rev: v6.0.0
hooks:
- id: check-added-large-files
- id: check-case-conflict
- id: check-executables-have-shebangs
- id: check-json
- id: check-merge-conflict
- id: check-shebang-scripts-are-executable
- id: check-symlinks
- id: check-vcs-permalinks
- id: check-yaml
- id: destroyed-symlinks
- id: detect-private-key
- id: fix-byte-order-marker
- id: file-contents-sorter
- id: check-added-large-files
- id: check-case-conflict
- id: check-executables-have-shebangs
- id: check-json
- id: check-merge-conflict
- id: check-shebang-scripts-are-executable
- id: check-symlinks
- id: check-vcs-permalinks
- id: check-yaml
- id: destroyed-symlinks
- id: detect-private-key
- id: fix-byte-order-marker
- id: file-contents-sorter
args: [--unique]
files: '\.epubcheck\.tsv|\.htmlvalidateignore'
- id: forbid-new-submodules
- id: end-of-file-fixer
- id: mixed-line-ending
- id: trailing-whitespace
- id: forbid-new-submodules
- id: end-of-file-fixer
- id: mixed-line-ending
- id: trailing-whitespace
- repo: https://github.com/igorshubovych/markdownlint-cli
rev: v0.47.0
hooks:
- id: markdownlint
files: 'src/.*\.md'
10 changes: 7 additions & 3 deletions courses/TSPL/2019/Assignment1.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ title : "Assignment1: TSPL Assignment 1"
permalink : /TSPL/2019/Assignment1/
---

```
```agda
module Assignment1 where
```

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

Submit your homework using the "submit" command.

```bash
submit tspl cw1 Assignment1.lagda.md
```

Please ensure your files execute correctly under Agda!


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

## Imports

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

A more efficient representation of natural numbers uses a binary
rather than a unary system. We represent a number as a bitstring.
```

```agda
data Bin : Set where
nil : Bin
x0_ : Bin → Bin
x1_ : Bin → Bin
```

For instance, the bitstring

1011
Expand Down
Loading
Loading