Jesse Wright 0055baf73a doc: add links to folder references (#3249) ... This PR adds links to some folder references in the docs, making them easier to navigate. Please advise if these need to be made to be full URIs rather than relative paths in order to work correctly with the doc generation tooling that is in place.		2024-02-05 13:30:48 +00:00
..
bin	chore: update domain	2023-09-20 15:13:27 -07:00
dev	doc: add links to folder references (#3249)	2024-02-05 13:30:48 +00:00
examples	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
images	doc: update quickstart guide to reference vs code setup guide (#2968)	2023-12-12 08:36:27 +00:00
latex	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
make	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00
monads	chore: fix more typos in comments	2023-10-08 14:37:34 -07:00
.gitignore	doc: mdbook init	2020-10-30 14:23:47 +01:00
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: remove Bootstrap package	2022-09-02 16:39:03 -07:00
builtintypes.md	doc: builtin types	2020-12-08 10:09:58 -08:00
char.md	doc: builtin types	2020-12-08 10:09:58 -08: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	doc: basic documentation	2020-11-18 18:47:22 -08:00
dep.md	fix: docs	2021-06-29 22:14:16 -07:00
deptypes.md	doc: add deptypes section	2020-12-07 13:58:52 -08:00
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	feat: partial context info (#3159)	2024-01-22 12:34:20 +00:00
flake.nix	feat: partial context info (#3159)	2024-01-22 12:34:20 +00:00
float.md	doc: builtin types	2020-12-08 10:09:58 -08:00
fplean.md	chore: update domain	2023-09-20 15:13:27 -07:00
funabst.md	doc: minor edits	2020-12-22 18:54:57 +01:00
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: minor edits	2020-12-22 18:54:57 +01:00
introdef.md	doc: add deptypes section	2020-12-07 13:58:52 -08:00
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	doc: builtin types	2020-12-08 10:09:58 -08:00
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	fix: namespaces.md	2020-11-20 07:56:53 -08:00
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	doc: builtin types	2020-12-08 10:09:58 -08:00
organization.md	doc: implicit arguments	2020-12-07 16:12:16 -08:00
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 to reference vs code setup guide (#2968)	2023-12-12 08:36:27 +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	doc: remove nightly and other outdated references (#3027)	2024-01-25 13:53:36 +00:00
simptypes.md	doc: minor edits	2020-12-22 18:54:57 +01:00
string.md	doc: builtin types	2020-12-08 10:09:58 -08:00
stringinterp.md	chore: cleaner structure/class syntax	2020-11-24 13:07:43 -08:00
struct.md	doc: structure update	2021-12-15 11:48:46 +00:00
SUMMARY.md	doc: remove Nix docs	2023-12-01 08:32:20 +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: explain how to use custom lexers in the latest minted (#3047)	2023-12-11 09:16:40 +00:00
tactics.md	doc: fix typos (#2160)	2023-03-22 10:01:59 +01:00
task.md	doc: builtin types	2020-12-08 10:09:58 -08:00
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	doc: builtin types	2020-12-08 10:09:58 -08:00
unifhint.md	doc: structures	2020-12-08 16:25:19 -08:00
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