michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update README/usage

Browse source
This commit is contained in:
Floris van Doorn 2018-10-03 13:42:09 -04:00
parent 3b25ec0266
commit 138fef02fa
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
README.md
View file

@ -112,8 +112,9 @@ These projects are done
+ need to splice together LES's + need to splice together LES's
## Usage and Contributing ## Usage and Contributing
- To compile this repository you will need a working version of Lean 2. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2). - To compile this repository you can run `linja` (or `path/to/lean2/bin/linja`) in the main directory.
- We will try to make sure that this repository compiles with the newest version of Lean 2. + You will need a working version of Lean 2. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2).
- Some notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot). + We will try to make sure that this repository compiles with the newest version of Lean 2.
- The preferred editor for Lean 2 is Emacs. Notes on the Emacs mode can be found [here](https://github.com/leanprover/lean2/blob/master/src/emacs/README.md) (for example if some unicode characters don't show up, or increase the spacing between lines by a lot).
- We try to separate the repository into the folders `algebra`, `homotopy`, `homology`, `cohomology`, `spectrum` and `colimit`. Homotopy theotic properties of types which do not explicitly mention homotopy, homology or cohomology groups (such as `A ∧ B ≃* B ∧ A`) are part of `homotopy`. - We try to separate the repository into the folders `algebra`, `homotopy`, `homology`, `cohomology`, `spectrum` and `colimit`. Homotopy theotic properties of types which do not explicitly mention homotopy, homology or cohomology groups (such as `A ∧ B ≃* B ∧ A`) are part of `homotopy`.
- If you contribute, please use rebase instead of merge (e.g. `git pull -r`). - If you contribute, please use rebase instead of merge (e.g. `git pull -r`).