michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8744 commits 3 branches 0 tags 28 MiB
Commit graph

34 commits

Author SHA1 Message Date
Ramana Kumar
7596ea285e fix(doc/lean/tutorial): correct some typos and infelicities in the short tutorial 2016-11-02 10:37:06 -07:00
Jeremy Avigad
d773302c6b chore(doc/lean/tutorial.org): comment out old rewriter information 2016-05-06 14:15:51 -07: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
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
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
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