Skip to content

part1/Relations: add product import #388

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wadler merged 2 commits into from
Aug 26, 2019
Merged

part1/Relations: add product import #388

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
aaf5b91
part1/Relations: Fix Typo
trajafri Aug 26, 2019
bb5ff4c
part1/Relations: Add _*_ import
trajafri Aug 26, 2019
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
4 changes: 2 additions & 2 deletions src/plfa/part1/Relations.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ the next step is to define relations, such as _less than or equal_.
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm)
```

Expand Down Expand Up @@ -161,7 +161,7 @@ Chapter [Decidable]({{ site.baseurl }}/Decidable/).
## Inversion

In our defintions, we go from smaller things to larger things.
For instance, form `m ≤ n` we can conclude `suc m ≤ suc n`,
For instance, from `m ≤ n` we can conclude `suc m ≤ suc n`,
where `suc m` is bigger than `m` (that is, the former contains
the latter), and `suc n` is bigger than `n`. But sometimes we
want to go from bigger things to smaller things.
Expand Down