Leonardo de Moura d46d246cd9 fix: documentation		2022-02-15 16:19:35 -08:00
..
bin
dev	chore: remove leanpkg	2022-02-04 19:03:40 +01:00
examples/compiler
images
latex
make
tutorial
.gitignore
array.md
autobound.md	chore: fix doc	2022-02-10 17:12:18 -08:00
book.toml
bool.md
BoolExpr.lean
builtintypes.md
char.md
declarations.md	fix: documentation	2022-02-15 16:19:35 -08:00
decltypes.md
definitions.md
dep.md
deptypes.md
do.md	doc: document some do block patterns/sugar	2022-02-07 20:50:15 +01:00
enum.md
expressions.md	doc: document some do block patterns/sugar	2022-02-07 20:50:15 +01:00
faq.md
float.md
funabst.md
functions.md
highlight.js
implicit.md
inductive.md
int.md
introdef.md
lean3changes.md
lexical_structure.md
list.md
macro_overview.md
metaprogramming.md
mission.md
namespaces.md
nat.md
notation.md
option.md
organization.md
other_commands.md
perf.md
quickstart.md	doc: replace leanpkg info with info about Lake	2021-12-19 17:23:25 +01:00
sections.md
setup.md	chore: remove leanpkg	2022-02-04 19:03:40 +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
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
typeclass.md	chore: fix doc	2022-01-16 09:28:03 -08:00
typeobjs.md
types.md
uint.md
unifhint.md
using_lean.md
whatIsLean.md