Floris van Doorn
|
97065119b0
|
doc(ubuntu-12.04-detailed): update installation instructions
|
2017-01-18 22:25:26 +01:00 |
|
Ramana Kumar
|
7596ea285e
|
fix(doc/lean/tutorial): correct some typos and infelicities in the short tutorial
|
2016-11-02 10:37:06 -07:00 |
|
Daniel Selsam
|
c6726d22ec
|
doc(export_format): minor fixes
|
2016-05-06 14:20:19 -07:00 |
|
Jeremy Avigad
|
d773302c6b
|
chore(doc/lean/tutorial.org): comment out old rewriter information
|
2016-05-06 14:15:51 -07:00 |
|
Daniel Selsam
|
8f0a0d2b32
|
feat(library/export, doc/export_format): remove support for mutually inductive types
|
2016-03-10 20:22:47 -08:00 |
|
Leonardo de Moura
|
d84a20d68b
|
remove(frontends/lean/server): FINDG command
|
2016-03-03 10:12:24 -08:00 |
|
Sebastian Ullrich
|
2a35c0f49b
|
feat(script): add .md link checker script
|
2016-02-23 10:11:24 -08:00 |
|
Leonardo de Moura
|
f67181baf3
|
chore(*): remove support for Lua
|
2016-02-11 17:17:55 -08:00 |
|
Jeremy Avigad
|
e14a2aaf3c
|
feat(doc/lean/library_style.org): clarify C_of_A_of_B convention
|
2015-12-31 15:16:57 -08:00 |
|
Leonardo de Moura
|
b36ce49f2b
|
fix(tests,doc): adjust tests to changes in the standard library
|
2015-12-05 23:52:16 -08:00 |
|
Leonardo de Moura
|
c280ddb2b0
|
fix(tests,doc): adjust tests and documentation
|
2015-11-20 17:03:17 -08:00 |
|
Leonardo de Moura
|
6df31d3406
|
refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading
|
2015-11-08 14:04:56 -08:00 |
|
Leonardo de Moura
|
4e78e35f77
|
fix(tests/lean): adjust remaining tests to changes in the standard library
|
2015-11-08 14:04:56 -08:00 |
|
Daniel Selsam
|
0715c86ff4
|
fix(library/export): closes #841
|
2015-10-05 10:11:04 -07:00 |
|
Leonardo de Moura
|
d140ff6148
|
fix(doc/lua/lua.md): adjust test to reflect recent changes in the expr caching mechanism
|
2015-09-30 17:34:39 -07:00 |
|
Leonardo de Moura
|
49eb7166f0
|
refactor(library/data): rename fixed_list -> tuple
|
2015-08-13 16:45:34 -07:00 |
|
Leonardo de Moura
|
d2eb99bf11
|
refactor(library/logic): move logic/choice.lean to init/classical.lean
choice axiom is now in the classical namespace.
|
2015-08-12 18:37:33 -07:00 |
|
Leonardo de Moura
|
b4024982a2
|
refactor(library/data): move vector as indexed family to examples folder
|
2015-08-12 15:05:14 -07:00 |
|
Théo Zimmermann
|
698b368f01
|
fix(doc): fix confusion between Prop and Bool
this fix assumes that Prop and Bool are two different things but even if they were the same thing, using the two names would only confuse the reader
|
2015-07-30 10:21:43 -07:00 |
|
Théo Zimmermann
|
923d12553e
|
fix(doc): correct two more mistakes
- fix a mistake in code example
- fix singular/plural confusion
|
2015-07-30 10:21:42 -07:00 |
|
Théo Zimmermann
|
3598a6610f
|
fix(doc): add missing words to fix meaning
|
2015-07-30 10:21:42 -07:00 |
|
Théo Zimmermann
|
b5432d4d3b
|
fix(doc): corrects language mistakes
corrects two confusions between singular and plural
|
2015-07-30 10:21:42 -07:00 |
|
Théo Zimmermann
|
c4e48a184c
|
fix(doc): fix subsection title
expand "(disjunction)" title for consistency with the other subsection titles around
|
2015-07-30 10:21:42 -07:00 |
|
Théo Zimmermann
|
dd0a8b7743
|
fix(doc): remove misplaced capital letter
|
2015-07-30 10:21:42 -07:00 |
|
Théo Zimmermann
|
7202e076dd
|
fix(doc): correct language mistakes
|
2015-07-30 10:21:42 -07:00 |
|
Leonardo de Moura
|
bbd6946a15
|
refactor(library/logic/axioms): we have only one extra axiom
|
2015-07-29 13:36:23 -07:00 |
|
Leonardo de Moura
|
6805aab344
|
feat(doc/export_format): update documentation
|
2015-07-28 16:04:11 -07:00 |
|
Daniel Selsam
|
ee11fca69b
|
refactor(src/library/export): disambiguate export keywords
|
2015-07-27 19:08:26 -07:00 |
|
Daniel Selsam
|
214b5b8b58
|
refactor(src/library/export): prefix export keywords with #
|
2015-07-27 15:07:12 -07:00 |
|
Leonardo de Moura
|
fa7a527590
|
feat(doc/make/msys2): add emacs-dependencies
|
2015-07-20 17:32:20 -07:00 |
|
Leonardo de Moura
|
7e0844a9e6
|
fix(tests): to reflect recent changes in the standard library
|
2015-07-06 15:05:01 -07:00 |
|
Leonardo de Moura
|
7940889495
|
fix(doc/lean/library_style): adjust to reflect changes in the standard library
|
2015-06-16 11:29:17 -07:00 |
|
Leonardo de Moura
|
375997fe65
|
fix(doc/lean/library_style): adjust to reflect changes in the standard library
|
2015-05-25 16:56:00 -07:00 |
|
Jeremy Avigad
|
5ae63c07a6
|
fix(doc/lean/library_style.org): remove unnecessary header line
|
2015-05-16 17:53:35 +10:00 |
|
Jeremy Avigad
|
0eb52e1f8b
|
fix(doc/library_style.org): use org format for headers
|
2015-05-13 22:19:02 -07:00 |
|
Soonho Kong
|
651345a89b
|
doc(make/msys2.md): remove msys2's Python, add how to install native one
[skip ci]
|
2015-05-12 13:03:51 -04:00 |
|
Leonardo de Moura
|
22a0e80ae8
|
fix(doc/lean/library_style): fix more code snippets
|
2015-05-12 06:42:41 -07:00 |
|
Leonardo de Moura
|
5cde3d5c1c
|
fix(doc/lean/library_style): code snippets must be valid Lean code
The test suite executes all code snippets in .org files and report errors.
|
2015-05-12 06:38:16 -07:00 |
|
Jeremy Avigad
|
b2dd95114b
|
feat(doc/lean/library_style.org,README.md): add library style conventions
|
2015-05-12 06:20:51 -07:00 |
|
Leonardo de Moura
|
57ea660963
|
refactor(*): start process for eliminating of opaque definitions from the kernel
see issue #576
|
2015-05-08 16:06:04 -07:00 |
|
Leonardo de Moura
|
2405ce34de
|
doc(export_format): document low level export format
|
2015-05-04 19:37:39 -07:00 |
|
Soonho Kong
|
8243ed6339
|
fix(test*.sh): allow spaces in filename
fix #515
|
2015-03-28 23:29:52 -04:00 |
|
Soonho Kong
|
0d1da89cf1
|
chore(.gitignore): update
|
2015-03-28 23:29:41 -04:00 |
|
Leonardo de Moura
|
cbac8d1300
|
chore(README): avoid duplication
|
2015-03-28 16:23:32 -07:00 |
|
Leonardo de Moura
|
61cdec73f6
|
chore(doc/lean/lexical): remove obsolete documentation from Lean 0.1
|
2015-03-06 14:22:05 -08:00 |
|
Leonardo de Moura
|
daf27fd194
|
doc(fixing_tests): add links to directories containing tests that compare produced vs expected output
|
2015-02-25 14:04:17 -08:00 |
|
Soonho Kong
|
eec57bef33
|
doc(syntax_highlight_in_latex.md): use bitbucket.org/leanprover/pygments-main
[skip ci]
|
2015-02-17 11:47:35 -05:00 |
|
Leonardo de Moura
|
f53a956a28
|
fix(doc/lean/expr): remove obsolete documentation
It is subsumed by the Lean tutorial.
closes #431
|
2015-02-12 18:03:57 -08:00 |
|
Leonardo de Moura
|
c3b4ed8267
|
doc(fixing_tests.md): add documentation for fixing broken tests
|
2015-02-01 11:55:33 -08:00 |
|
Leonardo de Moura
|
b4d6f6e3ed
|
feat(frontends/lean): 'attribute' command is persistent by default
|
2015-01-26 11:51:17 -08:00 |
|