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 doc: fix overwide view when using Alectryon 2022-06-23 18:23:28 +02:00
alectryon.js doc: embed examples into doc book 2022-04-06 09:06:49 -07:00
array.md doc: add new example 2022-07-09 17:04:08 -07:00
autobound.md doc: Semantic highlighting 2022-10-02 08:37:15 -07:00
book.toml doc: fold sub-chapters by default 2022-04-20 18:46:30 +02:00
bool.md chore: CRLF be gone 2021-11-09 09:49:09 +01:00
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 doc: fix typos 2021-03-07 15:06:02 +01:00
definitions.md
dep.md fix: docs 2021-06-29 22:14:16 -07:00
deptypes.md
do.md doc: document some do block patterns/sugar 2022-02-07 20:50:15 +01:00
elaborators.md doc: clean up syntax ToC 2022-04-26 18:58:45 +02:00
enum.md doc: "enumerated types" section markdown fix 2021-05-06 17:04:51 +02:00
examples.md doc: embed examples into doc book 2022-04-06 09:06:49 -07:00
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 chore: prune ancient keywords 2022-08-01 13:32:56 +02:00
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 refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
metaprogramming-arith.md doc: update link target (#3218) 2024-01-26 10:20:22 +00:00
mission.md doc: start porting reference manual 2021-08-27 19:30:08 -07:00
namespaces.md
nat.md doc: typo 2021-01-10 10:51:00 +01:00
notation.md feat: reduce precedence of unary neg 2022-11-06 18:13:48 -08:00
option.md
organization.md
other_commands.md doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00
perf.md doc: add basic perf documentation 2021-09-06 07:12:36 -07:00
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 doc: correct typo “command instruct” ->”command instructs” 2021-07-03 11:22:04 +02:00
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 doc: structure update 2021-12-15 11:48:46 +00:00
SUMMARY.md feat: checklist for release process (#3536) 2024-03-05 02:55:17 +00:00
syntax.md doc: clean up syntax ToC 2022-04-26 18:58:45 +02:00
syntax_example.lean doc: fix example style 2022-04-22 16:26:16 +02:00
syntax_example.md doc: fix example style 2022-04-22 16:26:16 +02:00
syntax_examples.md doc: missing file 2022-04-20 19:13:53 +02:00
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 doc: fix trivial typo 2022-01-09 10:19:26 +01:00
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 doc: fix typos 2021-03-07 15:06:02 +01:00
types.md chore: CRLF be gone 2021-11-09 09:49:09 +01:00
uint.md
unifhint.md
using_lean.md doc: start porting reference manual 2021-08-27 19:30:08 -07:00
whatIsLean.md fix: broken internal links in the docs (#3216) 2024-01-25 09:56:20 +00:00