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
|
7e0844a9e6
|
fix(tests): to reflect recent changes in the standard library
|
2015-07-06 15:05:01 -07:00 |
|
Jeremy Avigad
|
486bc321ff
|
refactor(library/data/nat): rename theorems
|
2014-12-23 21:14:35 -05:00 |
|
Leonardo de Moura
|
5cf8064269
|
refactor(library): rename exists_elim and exists_intro to exists.elim
and exists.intro
|
2014-12-15 19:07:38 -08:00 |
|
Jeremy Avigad
|
3e9a484851
|
refactor(library/logic/connectives): rename theorems
|
2014-12-15 15:05:44 -05:00 |
|
Leonardo de Moura
|
4946f55290
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-10-02 17:55:34 -07:00 |
|
Leonardo de Moura
|
e64d5c4a4a
|
refactor(library/data/nat): use new operator '!'
|
2014-10-01 18:39:47 -07:00 |
|
Leonardo de Moura
|
6632a50015
|
refactor(library): add namespaces 'or', 'and' and 'iff'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 21:25:21 -07:00 |
|
Leonardo de Moura
|
68d9bef860
|
refactor(library): add 'eq' and 'ne' namespaces
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 18:41:06 -07:00 |
|
Leonardo de Moura
|
2bc6f92d33
|
refactor(library): add 'and' namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:44:53 -07:00 |
|
Leonardo de Moura
|
364bba2129
|
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:26:36 -07:00 |
|
Leonardo de Moura
|
e51c4ad2e9
|
feat(frontends/lean): rename 'using' command to 'open'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-03 16:00:38 -07:00 |
|
Leonardo de Moura
|
6b7e79b62f
|
feat(library/data/nat): mark more arguments implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-28 10:38:58 -07:00 |
|
Leonardo de Moura
|
2d78387541
|
refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-27 18:34:09 -07:00 |
|
Leonardo de Moura
|
a8d58fdd33
|
refactor(library): mark absurd_elim argument as implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-26 18:27:39 -07:00 |
|
Leonardo de Moura
|
800d3bd70a
|
fix(doc/lean/tutorial): typos
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-25 11:22:15 -07:00 |
|
Leonardo de Moura
|
8375626cb6
|
fix(doc/lean/tutorial): adjust tutorial to library changes, fix test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-20 18:32:53 -07:00 |
|
Leonardo de Moura
|
8e6324185a
|
fix(tests/lean): adjust tests to new library structure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-01 09:37:23 -07:00 |
|
Leonardo de Moura
|
105c29b51e
|
refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-28 19:59:38 -07:00 |
|
Leonardo de Moura
|
2b4bd66081
|
feat(build): generate tests for all code blocks in org-files, and examples at ./examples/standard
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-28 12:06:11 -07:00 |
|
Leonardo de Moura
|
8ad6d7a98b
|
doc(doc/lean): update Lean tutorial to Lean 0.2, and use org-mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-28 10:52:09 -07:00 |
|