lean4-htt/doc
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 chore: update domain 2023-09-20 15:13:27 -07:00
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 doc: Semantic highlighting 2022-10-02 08:37:15 -07:00
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
dep.md
deptypes.md
do.md
elaborators.md
enum.md
examples.md
expressions.md doc: fix typos (#2160) 2023-03-22 10:01:59 +01:00
faq.md doc: fix the link to contribution guidelines (#2623) 2023-10-05 12:02:55 +11:00
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 chore: update domain 2023-09-20 15:13:27 -07:00
funabst.md
functions.md fix: broken internal links in the docs (#3216) 2024-01-25 09:56:20 +00:00
highlight.js fix: highlight of deriving instance (#1717) 2022-10-12 14:24:16 -07:00
implicit.md
inductive.md chore: update domain 2023-09-20 15:13:27 -07:00
int.md doc: fix integer division example 2024-07-19 10:36:43 +02:00
introdef.md
lean3changes.md chore: expand remark 2023-05-05 12:21:32 -07:00
lexical_structure.md feat: Rust-style raw string literals (#2929) 2023-12-20 16:53:08 +00:00
list.md
macro_overview.md doc: fix typos (#2160) 2023-03-22 10:01:59 +01:00
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 feat: reduce precedence of unary neg 2022-11-06 18:13:48 -08:00
option.md
organization.md
other_commands.md
perf.md
pygments.css doc: add documentation on monads (#1505) 2022-09-05 13:33:15 -07:00
quickstart.md doc: update quickstart guide for new display name (#5193) 2024-08-28 13:29:16 +00:00
sections.md
semantic_highlighting.md chore: update domain 2023-09-20 15:13:27 -07:00
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 doc: fix typos (#2160) 2023-03-22 10:01:59 +01:00
task.md
thunk.md
tour.md fix: broken internal links in the docs (#3216) 2024-01-25 09:56:20 +00:00
tpil.md chore: update domain 2023-09-20 15:13:27 -07:00
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