lean4-htt/doc
Sebastian Ullrich 119f685cda
doc: fix link
2021-08-08 18:39:28 +02:00
..
bin
examples/compiler
images doc: quickstart 2021-04-06 17:34:01 +02:00
latex doc: bundle updated lean4.py Pygments file and lstlean.tex 2021-07-12 11:33:13 -07:00
make doc: less Emacs-centric 2021-05-18 21:08:53 +02:00
.gitignore
array.md doc: fix typos (#379) 2021-04-30 19:36:30 +02:00
autobound.md fix: docs 2021-06-29 22:14:16 -07:00
book.toml
BoolExpr.lean doc: add example 2021-03-31 08:13:22 -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
coding_style.md
commit_convention.md
debugging.md doc: update dbg_trace docs 2021-04-23 15:48:43 +02: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 doc: add deptypes section 2020-12-07 13:58:52 -08:00
do.md doc: fix typo in the manual 2021-07-10 10:35:51 +02:00
enum.md doc: "enumerated types" section markdown fix 2021-05-06 17:04:51 +02:00
faq.md doc: clarify RFC issues 2021-06-04 14:12:59 +02:00
fixing_tests.md doc: fix typos 2021-03-07 15:06:02 +01:00
float.md doc: builtin types 2020-12-08 10:09:58 -08:00
funabst.md doc: minor edits 2020-12-22 18:54:57 +01:00
functions.md doc: fix typos 2021-03-07 15:06:02 +01:00
highlight.js fix: docs 2021-06-29 22:14:16 -07:00
implicit.md doc: replace variables 2021-01-22 18:38:49 +01:00
inductive.md doc: structures 2020-12-08 16:25:19 -08: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 doc: fix typos 2021-03-07 15:06:02 +01:00
list.md doc: builtin types 2020-12-08 10:09:58 -08:00
mdbook.md
namespaces.md
nat.md doc: typo 2021-01-10 10:51:00 +01: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
quickstart.md doc: direct link & instructions for elan on Windows 2021-06-01 16:38:03 +02:00
sections.md doc: correct typo “command instruct” ->”command instructs” 2021-07-03 11:22:04 +02:00
setup.md doc: fix link 2021-08-08 18:39:28 +02: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
struct.md doc: fix typos 2021-03-07 15:06:02 +01:00
SUMMARY.md doc: add quickstart to SUMMARY 2021-04-06 17:48:28 +02:00
syntax.md doc: link to some macro documentation 2021-08-08 12:41:59 +02:00
syntax_highlight_in_latex.md doc: bundle updated lean4.py Pygments file and lstlean.tex 2021-07-12 11:33:13 -07:00
tactics.md chore: fix docs 2021-08-08 13:26:46 +02:00
task.md doc: builtin types 2020-12-08 10:09:58 -08:00
test
thunk.md chore: fix doc 2021-03-11 11:40:39 -08:00
tour.md chore: fix typos 2021-01-20 22:43:25 +01:00
typeclass.md doc: fix typos (#379) 2021-04-30 19:36:30 +02:00
typeobjs.md doc: fix typos 2021-03-07 15:06:02 +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
whatIsLean.md doc: minor edits 2020-12-22 18:54:57 +01:00