| .. |
|
bin
|
|
|
|
dev
|
chore: symlink to source from build dir
|
2021-11-19 10:09:26 +01:00 |
|
examples/compiler
|
|
|
|
images
|
doc: add wsl setup docs and reorganize a new "dev" folder
|
2021-09-23 09:21:39 +02:00 |
|
latex
|
|
|
|
make
|
doc: advise using Developer Mode on Windows
|
2021-11-19 10:09:26 +01:00 |
|
tutorial
|
feat: allow more atoms starting with "`"
|
2021-10-19 14:10:31 +02:00 |
|
.gitignore
|
|
|
|
array.md
|
|
|
|
autobound.md
|
|
|
|
book.toml
|
|
|
|
bool.md
|
chore: CRLF be gone
|
2021-11-09 09:49:09 +01:00 |
|
BoolExpr.lean
|
|
|
|
builtintypes.md
|
|
|
|
char.md
|
|
|
|
declarations.md
|
doc: fix some syntax and link in the docs, and more
|
2021-10-10 11:36:43 +02:00 |
|
decltypes.md
|
|
|
|
definitions.md
|
|
|
|
dep.md
|
|
|
|
deptypes.md
|
|
|
|
do.md
|
feat: in pure code, do use assume Id monad at do notation
|
2021-12-10 12:55:14 -08:00 |
|
enum.md
|
|
|
|
expressions.md
|
doc: fix some syntax and link in the docs, and more
|
2021-10-10 11:36:43 +02:00 |
|
faq.md
|
doc: faq: bullet points look weird and are not anchors
|
2021-12-09 11:53:25 +01:00 |
|
float.md
|
|
|
|
funabst.md
|
|
|
|
functions.md
|
|
|
|
highlight.js
|
|
|
|
implicit.md
|
|
|
|
inductive.md
|
|
|
|
int.md
|
|
|
|
introdef.md
|
|
|
|
lean3changes.md
|
|
|
|
lexical_structure.md
|
doc: fix some syntax and link in the docs, and more
|
2021-10-10 11:36:43 +02:00 |
|
list.md
|
|
|
|
macro_overview.md
|
doc: add/edit macro guide
|
2021-11-22 11:02:07 +01:00 |
|
metaprogramming.md
|
doc: add macro guide, light reorganizing
|
2021-11-22 11:02:07 +01:00 |
|
mission.md
|
|
|
|
namespaces.md
|
|
|
|
nat.md
|
|
|
|
notation.md
|
doc: add macro guide, light reorganizing
|
2021-11-22 11:02:07 +01: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
|
|
|
|
quickstart.md
|
doc: replace leanpkg info with info about Lake
|
2021-12-19 17:23:25 +01:00 |
|
sections.md
|
|
|
|
setup.md
|
doc: replace leanpkg info with info about Lake
|
2021-12-19 17:23:25 +01:00 |
|
simptypes.md
|
|
|
|
string.md
|
|
|
|
stringinterp.md
|
|
|
|
struct.md
|
doc: structure update
|
2021-12-15 11:48:46 +00:00 |
|
SUMMARY.md
|
chore(doc): remove duplicate Tactics section (#927)
|
2022-01-06 14:03:15 -08:00 |
|
syntax.md
|
doc: correct the link to "Lean Together 2021: Metaprogramming in Lean 4 continued"
|
2022-01-03 07:06:04 -08:00 |
|
syntax_example.md
|
doc: add/edit macro guide
|
2021-11-22 11:02:07 +01:00 |
|
syntax_highlight_in_latex.md
|
|
|
|
tactics.md
|
doc: document the split tactic
|
2022-01-04 13:28:36 -08:00 |
|
task.md
|
|
|
|
thunk.md
|
doc: fix trivial typo
|
2022-01-09 10:19:26 +01:00 |
|
tour.md
|
chore: fix doc
|
2021-09-16 10:32:00 -07:00 |
|
typeclass.md
|
chore: fix test
|
2021-11-15 18:47:25 -08:00 |
|
typeobjs.md
|
|
|
|
types.md
|
chore: CRLF be gone
|
2021-11-09 09:49:09 +01:00 |
|
uint.md
|
|
|
|
unifhint.md
|
|
|
|
using_lean.md
|
|
|
|
whatIsLean.md
|
doc: fix some syntax and link in the docs, and more
|
2021-10-10 11:36:43 +02:00 |
