Updated README with warning to use correct versions
This commit is contained in:
parent
9df5fbf827
commit
954d328a9d
2 changed files with 24 additions and 6 deletions
17
README.md
17
README.md
|
@ -17,20 +17,25 @@ There are several tools you need to work with PLFA:
|
||||||
- [Agda standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
|
- [Agda standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
|
||||||
|
|
||||||
For most of the tools, you can simply follow their respective build instructions.
|
For most of the tools, you can simply follow their respective build instructions.
|
||||||
We list the versions of our dependencies on the badges above.
|
We list the versions of our dependencies on the badges above. We have
|
||||||
|
tested with the versions listed; either earlier or later versions may
|
||||||
|
cause problems.
|
||||||
|
|
||||||
You can get the latest version of Programming Language Foundations in Agda from Github,
|
You can get the appropriate version of Programming Language Foundations in Agda from Github,
|
||||||
either by cloning the repository,
|
either by cloning the repository,
|
||||||
or by downloading [the zip archive](https://github.com/plfa/plfa.github.io/archive/dev.zip):
|
or by downloading [the zip archive](https://github.com/plfa/plfa.github.io/archive/dev.zip):
|
||||||
|
|
||||||
git clone https://github.com/plfa/plfa.github.io
|
git clone https://github.com/plfa/plfa.github.io
|
||||||
|
|
||||||
Finally, we need to let Agda know where to find the standard library.
|
Finally, we need to let Agda know where to find the standard library.
|
||||||
For this, you can follow the instructions [here](https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library).
|
For this, you can follow the instructions
|
||||||
|
[here](https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library).
|
||||||
|
|
||||||
It is possible to set up PLFA as an Agda library as well.
|
It is possible to set up PLFA as an Agda library as well. If you want
|
||||||
If you are trying to complete the exercises found in the `tspl` folder, or otherwise want to import modules from the book, you need to do this.
|
to complete the exercises found in the `courses` folder, or to import
|
||||||
To do so, add the path to `plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to `~/.agda/defaults`, both on lines of their own.
|
modules from the book, you need to do this. To do so, add the path to
|
||||||
|
`plfa.agda-lib` to `~/.agda/libraries` and add `plfa` to
|
||||||
|
`~/.agda/defaults`, both on lines of their own.
|
||||||
|
|
||||||
|
|
||||||
## Unicode characters
|
## Unicode characters
|
||||||
|
|
|
@ -130,6 +130,19 @@ same = extensionality (λ m → extensionality (λ n → same-app m n))
|
||||||
```
|
```
|
||||||
We occasionally need to postulate extensionality in what follows.
|
We occasionally need to postulate extensionality in what follows.
|
||||||
|
|
||||||
|
More generally, we may wish to postulate extensionality for
|
||||||
|
dependent functions.
|
||||||
|
```
|
||||||
|
postulate
|
||||||
|
∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
|
||||||
|
→ (∀ (x : A) → f x ≡ g x)
|
||||||
|
-----------------------
|
||||||
|
→ f ≡ g
|
||||||
|
```
|
||||||
|
Here the type of `f` and `g` has changed from `A → B` to
|
||||||
|
`∀ (x : A) → B x`, generalising ordinary functions to
|
||||||
|
dependent functions.
|
||||||
|
|
||||||
|
|
||||||
## Isomorphism
|
## Isomorphism
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue