max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/doc
History
Leonardo de Moura 2bc5b8d1ec chore: remove doc/changes.md 
In the last dev meeting, we have decided we are not going to use it.
We will release often (every month), and use pull requests and issues
to report changes.
2022-02-03 09:23:45 -08:00
..
bin chore(src/emacs): move lean-mode to https://github.com/leanprover/lean-mode 2017-10-06 10:46:43 -07:00
dev doc: more about initializers 2022-01-20 18:55:57 +01:00
examples/compiler chore: move tests to new frontend 2020-10-23 14:07:26 -07:00
images doc: add wsl setup docs and reorganize a new "dev" folder 2021-09-23 09:21:39 +02:00
latex doc: bundle updated lean4.py Pygments file and lstlean.tex 2021-07-12 11:33:13 -07:00
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 doc: mdbook init 2020-10-30 14:23:47 +01:00
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 doc: add # prefix to hide lines in lean code blocks 2020-10-30 16:00:20 +01:00
bool.md chore: CRLF be gone 2021-11-09 09:49:09 +01:00
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
declarations.md doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02: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 feat: in pure code, do use assume Id monad at do notation 2021-12-10 12:55:14 -08:00
enum.md doc: "enumerated types" section markdown fix 2021-05-06 17:04:51 +02:00
expressions.md doc: fix error in manual example 2022-01-22 10:03:32 +01:00
faq.md doc: faq: bullet points look weird and are not anchors 2021-12-09 11:53:25 +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
lexical_structure.md doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00
list.md doc: builtin types 2020-12-08 10:09:58 -08:00
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 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 doc: add macro guide, light reorganizing 2021-11-22 11:02:07 +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
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
quickstart.md doc: replace leanpkg info with info about Lake 2021-12-19 17:23:25 +01:00
sections.md doc: correct typo “command instruct” ->”command instructs” 2021-07-03 11:22:04 +02:00
setup.md chore: move out lean4-mode 2022-01-24 21:23:53 +01: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 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 doc: bundle updated lean4.py Pygments file and lstlean.tex 2021-07-12 11:33:13 -07:00
tactics.md doc: document the split tactic 2022-01-04 13:28:36 -08: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 chore: fix doc 2021-09-16 10:32:00 -07:00
typeclass.md chore: fix doc 2022-01-16 09:28:03 -08: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 doc: fix some syntax and link in the docs, and more 2021-10-10 11:36:43 +02:00