Sebastian Ullrich
2afbb2ce42
doc: fix
2020-12-09 11:07:02 +01:00
Leonardo de Moura
7705769139
doc: default instances and heterogeneous operators
2020-12-08 18:56:30 -08:00
Leonardo de Moura
4d6b80cd51
doc: structures
2020-12-08 16:25:19 -08:00
Leonardo de Moura
825bc3aa65
doc: array
2020-12-08 10:36:47 -08:00
Leonardo de Moura
1509a1ab18
doc: builtin types
2020-12-08 10:09:58 -08:00
Leonardo de Moura
eb11416edc
doc: auto bound implicit arguments
2020-12-07 16:38:55 -08:00
Leonardo de Moura
d4c67a6bf0
doc: implicit arguments
2020-12-07 16:12:16 -08:00
Leonardo de Moura
1c8432b814
doc: Type* as a macro
2020-12-07 15:14:52 -08:00
Leonardo de Moura
021d5804f8
doc: add deptypes section
2020-12-07 13:58:52 -08:00
Sebastian Ullrich
d96393ee47
doc: building Lean packages with Nix
2020-12-02 17:52:57 +01:00
Sebastian Ullrich
797bec86f5
chore: Nix: overhaul nix-dev, lift technical restrictions
2020-12-02 16:49:25 +01:00
Sebastian Ullrich
5adaecc00e
doc: Nix: more about nix develop
2020-12-01 15:55:41 +01:00
Leonardo de Moura
cde53c67e6
chore: fix docs
2020-11-29 20:09:32 -08:00
Leonardo de Moura
95736128aa
chore: fix doc/
2020-11-29 14:00:17 -08:00
Sebastian Ullrich
6f8d039c1b
doc: Nix: make binary cache setup compatible with Nix 2.3
2020-11-29 22:56:48 +01:00
Leonardo de Moura
7a622b2a85
chore: typo
2020-11-29 13:40:49 -08:00
Leonardo de Moura
707ff44066
doc: Thunk
...
TODO: `Task` and support for threads
2020-11-29 10:19:27 -08:00
Sebastian Ullrich
967c9c7d00
doc: Nix: debugging tip
2020-11-29 18:59:39 +01:00
Leonardo de Moura
ee77afafa5
doc: add typeclass.md
2020-11-26 08:42:42 -08:00
Sebastian Ullrich
45a315d273
doc: Nix: seems to work fine on macOS
2020-11-25 09:48:50 +01:00
Leonardo de Moura
46dfe7b911
doc: expand tactics.md
2020-11-24 16:56:09 -08:00
Leonardo de Moura
1aeb88cee5
feat: add where example in proofs
2020-11-24 16:30:28 -08:00
Leonardo de Moura
b72a3c69b6
fix: ambiguity at induction/cases
...
See efc3a320fe
2020-11-24 14:59:12 -08:00
Leonardo de Moura
5585f9823f
chore: cleaner structure/class syntax
...
@Kha I implemented the syntax for structure/class that we discussed this morning.
It is much cleaner. See new tests at `struct2.lean`.
I updated the documentation to use it.
2020-11-24 13:07:43 -08:00
Leonardo de Moura
cf0bb173ad
fix: highlight.js
2020-11-24 12:53:54 -08:00
Leonardo de Moura
fa04f46d55
doc: simplify begin..end macro
...
The method `getRef` returns the whole term being expanded.
@Kha The method was originially added for reporting error messages.
So, the name is counterintuitive.
2020-11-24 11:06:49 -08:00
Sebastian Ullrich
2c64441910
chore: Nix: disable dirty Git tree warning & fix lean4-diff-test-file
...
/cc @leodemoura
Note that you will have to restart Emacs and the "Lean shell" around it for the changes to take effect
2020-11-24 20:05:24 +01:00
Sebastian Ullrich
6be438d7b1
doc: Nix: more notes
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
4f89cbf9b9
doc: Nix: explain some warnings
...
/cc @leodemoura @javra
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
1b302f328f
doc: fix Bash comment highlighting
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
a5ad46f7be
feat: Nix: mdbook
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
ffb8e1904b
doc: Nix setup
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
e167085429
doc: remove outdated description
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
56d6bbbf05
doc: phrasing
2020-11-24 15:58:10 +01:00
Leonardo de Moura
a44e51ce2e
fix: identifiers highlighting and literals
2020-11-23 18:32:39 -08:00
Leonardo de Moura
0fc0bf0593
chore: use instance ... where in the docs
2020-11-23 18:30:21 -08:00
Leonardo de Moura
5b23efc112
chore: update FAQ
2020-11-23 10:19:15 -08:00
Leonardo de Moura
d5c7f91b83
chore: reorg manual main page
2020-11-23 09:58:51 -08:00
Leonardo de Moura
a297d4107e
doc: add tactics.md
2020-11-22 21:15:55 -08:00
Leonardo de Moura
9608ea5aef
doc: do notation
2020-11-22 16:15:33 -08:00
Leonardo de Moura
2a769bbd79
feat: add missing keywords
2020-11-20 09:45:36 -08:00
Sebastian Ullrich
f6943d9c13
doc: fix highlighting of #eval etc.
2020-11-20 16:59:23 +01:00
Sebastian Ullrich
1e2c0d1d41
doc: remove "section" keywords, which aren't highlighted
2020-11-20 16:59:23 +01:00
Sebastian Ullrich
23bedc5ef5
doc: inline un-minified highlightjs-lean code into highlight.js
2020-11-20 16:59:23 +01:00
Leonardo de Moura
40ab77288d
fix: namespaces.md
2020-11-20 07:56:53 -08:00
Leonardo de Moura
594c5a52f6
fix: sections.md
2020-11-19 19:06:06 -08:00
Leonardo de Moura
5fe11e0f00
doc: move example to tour.md
2020-11-19 17:38:51 -08:00
Leonardo de Moura
b619f09010
doc: section, variables and namespaces
2020-11-19 17:34:08 -08:00
Leonardo de Moura
e29cc367f3
feat: test each example using a separate file
2020-11-19 13:51:52 -08:00
Leonardo de Moura
72a6ce498a
chore: move lean3changes.md
2020-11-19 12:57:41 -08:00
