doc: fix typos (#2287)

This commit is contained in:
Pietro Monticone 2023-06-25 20:30:33 +02:00 committed by GitHub
parent 4036be4f50
commit fff4aea0d9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 4 additions and 4 deletions

View file

@ -818,7 +818,7 @@ v4.0.0-m4 (23 March 2022)
initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
```
If you don't neet to acces `my_ext`, you can also use the macro
If you don't need to access `my_ext`, you can also use the macro
```lean
import Lean

View file

@ -83,7 +83,7 @@ Work on two adjacent stages at the same time without the need for repeatedly upd
```bash
# open an editor that will use only committed changes (so first commit them when changing files)
nix run .#HEAD-as-stage1.emacs-dev&
# open a second editor that will use those commited changes as stage 0
# open a second editor that will use those committed changes as stage 0
# (so don't commit changes done here until you are done and ran a final `update-stage0-commit`)
nix run .#HEAD-as-stage0.emacs-dev&
```

View file

@ -212,7 +212,7 @@ so you get a nice zipped list like this:
-- [(1, 4), (2, 5), (3, 6)]
/-!
And of couse, as you would expect, there is an `unzip` also:
And of course, as you would expect, there is an `unzip` also:
-/
#eval List.unzip (List.zip [1, 2, 3] [4, 5, 6])
@ -286,7 +286,7 @@ But you will need to understand full Monads before this will make sense.
Diving a bit deeper, (you can skip this and jump to the [Applicative
Laws](laws.lean.md#what-are-the-applicative-laws) if don't want to dive into this implementation detail right
now). But, if you write a simple `Option` example `(.*.) <$> some 4 <*> some 5` that produces `some 20`
using `Seq.seq` you will see somthing interesting:
using `Seq.seq` you will see something interesting:
-/
#eval Seq.seq ((.*.) <$> some 4) (fun (_ : Unit) => some 5) -- some 20