https://github.com/leanprover/vscode-lean4/pull/521 changed the display
name of the VS Code extension so that it can be found more easily when
searching for "Lean" (before it would appear far down in the list). This
PR updates the quickstart guide to reflect this fact.
This PR updates the screenshots and instructions in the quickstart guide
for the most recent Lean 4 VS Code extension version and makes a small
stylistic change suggested by @semorrison.
Since the vscode-lean4 setup guide allows us to provide information on
setting up Lean 4 tailored to the user's operating system, this PR
adjusts the quickstart guide to reference the vscode-lean4 setup guide
instead.
* doc: add documentation on functors.
* fix: make comments green
* minor tweaks
* doc: add section on Applicatives.
* doc: add some more info on the laws from Mario.
* doc: add law list and move lazy evaluation up so the chapter ends properly.
* doc: Add something on seqLeft and seqRight.
* doc: add section on monads.
* doc: fix some typos.
* doc: switch to LeanInk for chaper on Monads.
* doc: remove old files.
* doc: fix mdbook test errors.
* doc: add part 4: readers
* doc: add section on State monads
* doc: fix some typos and add some more details.
* doc: fix typos and add some CR feedback.
* doc: add Except monad section.
* doc: add info on monad transformers.
* Delete transformers.lean.md
* doc: fix some typos.
* doc: fix typos and move forward reference to monad lifting.
* doc: Update `State` to `StateM`
* doc: fix references to State to become StateM.
* doc: generalize indexOf implementation.
* doc: add chapter on monad laws and move "law" sections to this chapter to avoid redundancy.
* doc: add theorem
* Delete laws.lean.md
* doc: fix some typos.
* doc: fix broken link.
* doc: fox typos.
* fix: language changed from "us" to "you".
* doc: fix code review comments.
* doc: some word smithing
* doc: some word smithing and sample simplification.
* doc: add bad_option_map example.
* doc: add side note on `return` statement and fix heading level consistency.
* Add `withReader` info
* doc: change language from us, our, your, we, we'll, we've to "you"
* doc: add some forward links.
* doc: put spaces around colon in function arguments like "(x : List Nat)"
* doc:
Add backticks on map
Remove commands on multiline structure instance
Fix centerdot
Add "one of"
* doc: Remove info about Functor in other languages.
* doc:
add info on <$> being left associative
remove another forward reference to monad
fix typo `operatoions`
remove unneccesary parens after <$>
* doc:
fix Type u -> Type v
fix you -> your
use `let val? ← IO.getEnv name`
in Readers call it "context" rather than "state".
* doc: fix withReader docs
use 'context' to describe the ReaderM state.
remove "trivial"
type inference => Lean
"abstract classes" => "abstract structures"
remove unnecessary parens
* doc: fix bug in explanation of `let x ← readerFunc2`
Fix explanation of equivalence between `def f (a : Nat) : String` and `def f : Nat → String`
* doc: move hasSomeItemGreaterThan to Except.lean
Add validateList List.anyM example.
fix `def f (a : Nat) : String` language.
* doc: fix "What transformation are you referring to"
* doc: fix typo.
* doc: add missing period.
* doc: fix validateList
* doc: explain `λ` notation.
* doc: reword the map, seq, bind comparison.
* doc: fix some more 'reader state' to 'reader context' language
* doc: fix wrote statement about return only works in do blocks.
* doc: fix typo
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* doc: improve language
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* doc: fix typo
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* Add info on what a do block is doing for you.
* doc: define definitionally equal
* doc: make `readerFunc3.run env` canonical.
* doc: remove unnecessary parens.
* doc: fix typos
* doc: make List.map a bit more clear in the intro to Functors.
* doc: simplify readerFunc3WithReader
* doc: switch to svg for diagram so it works better on dark themes.
* doc: align nodes in diagram and convert to svg.
* doc: simplify playGame using while true.
* doc: drop confusing statement about "definitionally equal"
* doc: switch to `import Lean.Data.HashMap`
* doc: fix typo "operatoins"
* doc: update diagram to add more info and polish the intro paragraphs so they better match the actual contents of each chapter.
* doc: fix typo
* doc: fix typo.
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
