Leonardo de Moura
7f00352d33
chore: backtick issue in documentation
2022-04-02 06:55:23 -07:00
Leonardo de Moura
e058fe65a9
feat: make the hypothesis name optional in the by_cases tactic
2022-04-01 19:36:13 -07:00
Leonardo de Moura
ed935ed7a7
doc: binary search trees
2022-04-01 19:30:28 -07:00
Leonardo de Moura
cfb4e306f7
refactor: replace length_dropLast theorem
2022-04-01 16:44:24 -07:00
Leonardo de Moura
df063a47fa
chore: fix link
2022-03-30 13:44:22 -07:00
Leonardo de Moura
b6ce9fa4b1
doc: add palindromes.lean
2022-03-30 11:22:58 -07:00
Leonardo de Moura
5ca9b49235
chore: cleanup proof
2022-03-28 14:58:02 -07:00
Leonardo de Moura
3c964f3b9f
feat: substitute auxiliary equations introduced by the split tactic
2022-03-28 14:29:28 -07:00
Leonardo de Moura
4e008cf8b7
chore: move to tests
2022-03-27 14:57:33 -07:00
Leonardo de Moura
a2c9b6a8be
chore: rename Substate => State.le
2022-03-27 09:30:55 -07:00
Leonardo de Moura
3fe7db1bbf
chore: remove dead theorem
2022-03-27 09:15:55 -07:00
Leonardo de Moura
b2ef678199
doc: constant propagation for simple imperative language
2022-03-27 09:02:37 -07:00
Leonardo de Moura
3b7c3c0017
chore: add TODO's
2022-03-26 18:59:43 -07:00
Leonardo de Moura
11ed51dcb2
doc: example for the tutorial
2022-03-26 18:52:53 -07:00
Sebastian Ullrich
85c7772f4c
doc: fix ReST markup
2022-03-26 22:50:04 +01:00
Sebastian Ullrich
bef34e30e7
feat: Nix: render examples using LeanInk+Alectryon
2022-03-26 22:50:04 +01:00
Sebastian Ullrich
282147631f
chore: Nix: add LeanInk + Alectyron to docs flake
2022-03-26 22:50:04 +01:00
Sebastian Ullrich
19925f8ec1
chore: Nix: move docs build into sub-flake
...
workflow is not ideal right now because of poor support for sub-flakes,
but I also don't want the doc input in the main flake...
2022-03-26 22:50:04 +01:00
Sebastian Ullrich
7ce5b0c4ff
feat: CI: build darwin_aarch64
2022-03-26 16:29:52 +01:00
Leonardo de Moura
6da9119516
doc: add Parametric Higher-Order Abstract Syntax example
2022-03-25 14:42:24 -07:00
Sebastian Ullrich
ca9678be58
doc: move tier list to setup.md
2022-03-25 17:45:15 +01:00
Leonardo de Moura
3c9556ec18
doc: finish deBruijn.lean example
2022-03-24 16:17:53 -07:00
Leonardo de Moura
52a52fbed7
chore: add doc/examples to the test suite
2022-03-24 15:20:18 -07:00
Arthur Paulino
53faa9c8ca
doc: restriction of partial functions
2022-03-24 15:01:50 -07:00
E.W.Ayers
90baf14e82
doc: add lib and style changes to lean3changes.md
2022-03-24 15:00:36 -07:00
Leonardo de Moura
170b911a6f
doc: expand deBruijn
2022-03-22 19:35:58 -07:00
Leonardo de Moura
20fb3e470d
doc: add dependent de Bruijn indices
...
TODO: explain example.
2022-03-22 19:11:06 -07:00
Leonardo de Moura
b2a1b88a4e
doc: a certified type checker
2022-03-22 19:01:26 -07:00
Leonardo de Moura
a23fcb6033
chore: use github link until we generate the proper webpage using Alectryon
2022-03-22 18:34:40 -07:00
Leonardo de Moura
028e3561e2
fix: link
2022-03-22 18:07:04 -07:00
Leonardo de Moura
265803f7ac
doc: fix links
2022-03-22 16:52:08 -07:00
Leonardo de Moura
e06893d1f2
doc: proper TPIL link
2022-03-22 16:37:16 -07:00
Leonardo de Moura
973b76a6e2
doc: add Examples section
2022-03-22 16:35:14 -07:00
Leonardo de Moura
412bc14fbe
doc: add well-typed interpreter as an example
2022-03-22 16:32:41 -07:00
Leonardo de Moura
5ae125262b
chore: remove C++ coding style from manual
2022-03-22 15:54:51 -07:00
Leonardo de Moura
2e9adf0e04
chore: remove broken documentation
2022-03-22 15:52:13 -07:00
Chris Lovett
6dc576121d
doc: replace quickstart leanpkg info with info about lake
2022-03-11 16:31:58 -08:00
Leonardo de Moura
272dd5533f
chore: style use · instead of . for lambda dot notation
...
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
2022-03-11 07:49:03 -08:00
Sebastian Ullrich
126c7dd4ea
chore: Nix: command for (one-time) linking .ileans
2022-03-09 10:29:25 +01:00
Leonardo de Moura
51ec4522fe
fix: documentation
2022-03-03 18:18:37 -08:00
Leonardo de Moura
d46d246cd9
fix: documentation
2022-02-15 16:19:35 -08:00
ammkrn
3de18ceb55
doc: document match h:e with syntax
2022-02-14 15:53:37 +01:00
Leonardo de Moura
a2b7ff9e0d
chore: fix doc
2022-02-10 17:12:18 -08:00
ammkrn
efb533fb24
doc: document some do block patterns/sugar
2022-02-07 20:50:15 +01:00
Sebastian Ullrich
a7ba103e0a
chore: remove leanpkg
2022-02-04 19:03:40 +01:00
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
Leonardo de Moura
9291f59c8f
chore: add changes.md
2022-01-31 15:52:28 -08:00
Sebastian Ullrich
b20ecd02d7
chore: move out lean4-mode
2022-01-24 21:23:53 +01:00
Tom Ball
0b140ea451
doc: fix error in manual example
...
Co-authored-by: Tom Ball <you@example.com>
2022-01-22 10:03:32 +01:00
Sebastian Ullrich
f0f26728ed
doc: more about initializers
2022-01-20 18:55:57 +01:00
