Marc Huisinga f220efc5ba doc: update quickstart guide for new display name (#5193) ... 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.		2024-08-28 13:29:16 +00:00
..
bin
dev	chore: begin development cycle for v4.12.0 (#4986)	2024-08-12 00:33:05 +00:00
examples	doc: update user widget manual (#5006)	2024-08-23 19:03:39 +00:00
images	doc: update quickstart guide for new display name (#5193)	2024-08-28 13:29:16 +00:00
latex	doc: upstream the Lean4 pygments lexer (#3125)	2024-05-20 11:40:24 +00:00
make	chore: add libuv to the required packages heading in macos docs (#5045)	2024-08-15 01:33:58 +00:00
monads	chore: Std -> Batteries renaming (#4108)	2024-05-08 05:04:25 +00:00
.gitignore
alectryon.css
alectryon.js
array.md
autobound.md
book.toml
bool.md
BoolExpr.lean	chore: Std -> Batteries renaming (#4108)	2024-05-08 05:04:25 +00:00
builtintypes.md
char.md	doc: documenting Char and upstreaming extensionality from batteries (#4438)	2024-06-16 00:43:34 +00:00
declarations.md	doc: mention termination_by and decreasing_by (#3016)	2024-01-10 16:35:19 +00:00
decltypes.md
definitions.md	doc: basic documentation	2020-11-18 18:47:22 -08:00
dep.md
deptypes.md
do.md
elaborators.md
enum.md
examples.md
expressions.md
faq.md
flake.lock	chore: deprecate Nix-based build, remove interactive components (#4895)	2024-08-02 09:57:34 +00:00
flake.nix	chore: deprecate Nix-based build, remove interactive components (#4895)	2024-08-02 09:57:34 +00:00
float.md
fplean.md
funabst.md
functions.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00
highlight.js
implicit.md
inductive.md
int.md	doc: fix integer division example	2024-07-19 10:36:43 +02:00
introdef.md
lean3changes.md
lexical_structure.md
list.md
macro_overview.md
metaprogramming-arith.lean
metaprogramming-arith.md	doc: update link target (#3218)	2024-01-26 10:20:22 +00:00
mission.md
namespaces.md
nat.md
notation.md
option.md
organization.md
other_commands.md
perf.md
pygments.css
quickstart.md	doc: update quickstart guide for new display name (#5193)	2024-08-28 13:29:16 +00:00
sections.md
semantic_highlighting.md
setup.md	chore: CI: native-compile aarch64 macOS (#4265)	2024-05-24 08:18:49 +00:00
simptypes.md
string.md
stringinterp.md
struct.md
SUMMARY.md	feat: checklist for release process (#3536)	2024-03-05 02:55:17 +00:00
syntax.md
syntax_example.lean
syntax_example.md
syntax_examples.md
syntax_highlight_in_latex.md	doc: upstream the Lean4 pygments lexer (#3125)	2024-05-20 11:40:24 +00:00
tactics.md
task.md
thunk.md
tour.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00
tpil.md
typeclass.md	doc: avoid universe issue in example type class code (#3098)	2023-12-21 16:57:26 +00:00
typeobjs.md
types.md
uint.md
unifhint.md
using_lean.md
whatIsLean.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00