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

88 commits

Author SHA1 Message Date
Leonardo de Moura
60a1ac3192 doc(cmake/osx10.8): add note regarding multi-thread support on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 12:43:40 -07:00
Leonardo de Moura
53ca4bc193 doc(doc/lua): add variable and lambda abstraction API documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 11:54:15 -07:00
Leonardo de Moura
54ec66709c doc(doc/lua): add constant and function application API documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 11:01:03 -07:00
Leonardo de Moura
38f471b390 doc(doc/lua): add universe polymorphism elimator example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-04 16:28:07 -07:00
Leonardo de Moura
a522398194 fix(doc/lua): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-04 15:06:44 -07:00
Leonardo de Moura
980eb2fa5c fix(doc/lua): typos in the documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 18:14:19 -07:00
Leonardo de Moura
5f3ac6287f fix(doc/lua): markup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 17:47:25 -07:00
Leonardo de Moura
c0b82412db doc(doc/lua): add universe level documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 17:36:07 -07:00
Leonardo de Moura
045a83153c doc(lua): update Lua API documentation, and reactivate doc tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 08:09:54 -07:00
Leonardo de Moura
7142c0fed3 doc(demo): remove Lean 0.1 demo files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:43:30 -07:00
Soonho Kong
4fddc5b8bc chore(travis): use lean-build@googlegroups 2014-05-02 17:21:54 -04:00
Leonardo de Moura
69bfc682b4 chore(*): replace leodemoura with leanprover 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 15:31:29 -07:00
Leonardo de Moura
ec27a70908 doc(*): update documentation and add link to Lean 0.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 11:00:49 -07:00
Leonardo de Moura
bbdf8bb68e doc(todo): update todo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:49:18 -07:00
Leonardo de Moura
0760b5b53d doc(todo): update todo list 2014-02-08 09:23:56 -08:00
Leonardo de Moura
ded72f94b2 doc(todo): update todo list 2014-02-08 09:23:13 -08:00
Leonardo de Moura
5454e2af32 doc(todo): remove item from todo list 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 15:04:10 -08:00
Leonardo de Moura
5efc60d1f1 doc(todo): add another item to todo list 2014-02-06 18:07:06 -08:00
Leonardo de Moura
45ef10e2c1 doc(todo): update todo list 2014-02-06 17:01:30 -08:00
Leonardo de Moura
ba9a8f9d98 feat(frontends/lean): add 'show' expression syntax sugar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 07:50:22 -08:00
Leonardo de Moura
cbe89ca32e doc(doc/todo): update TODO list 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:19:49 -08:00
Leonardo de Moura
17eb2374ee doc(README): add link to tutorial in the main page 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:14:02 -08:00
Leonardo de Moura
9fa03db42b doc(doc/lean/tutorial): expand the tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:09:55 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 19:28:42 -08:00
Leonardo de Moura
b55aee1efd doc(demo): add another example into demo set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 10:11:58 -08:00
Leonardo de Moura
9bdf076342 doc(demo): add files for making demos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 09:59:16 -08:00
Leonardo de Moura
ceff335bb8 doc(doc/lean/tutorial): update tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 22:58:44 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 17:39:12 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 16:54:21 -08:00
Leonardo de Moura
d83a13d044 doc(doc/lean/tutorial): update tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 21:56:08 -08:00
Leonardo de Moura
2179e57db3 refactor(builtin): move if_then_else to its own module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 14:08:39 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 08:33:52 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments 
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 19:10:30 -08:00
Leonardo de Moura
048151487e feat(kernel): use Pi as forall/implication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 00:38:39 -08:00
Leonardo de Moura
d9c41e7282 doc(lean): add tutorial draft, and fix lexical documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-07 00:06:32 -08:00
Leonardo de Moura
feae89d019 fix(doc/design): reflect changes in Lean syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:51:15 -08:00
Leonardo de Moura
62bb2ab2f9 fix(builtin/Nat): name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:41:14 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:41:03 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 19:21:44 -08:00
Leonardo de Moura
9d6bd7501c feat(doc/lean): include lean documentation scripts in the test set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 13:16:47 -08:00
Leonardo de Moura
028a9bd9bd feat(frontends/lean/scanner): use Lua style comments in Lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 08:53:27 -08:00
Leonardo de Moura
03cf9be8b5 doc(doc/lean/calc.md): link to Nat.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 11:59:24 -08:00
Leonardo de Moura
66ec538c63 doc(doc/lean/calc.md): calculational proof documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-03 11:52:21 -08:00
Leonardo de Moura
3874e23a76 doc(doc/lean): expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 21:29:54 -08:00
Leonardo de Moura
f27105d17f doc(doc/lean): lexical conventions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-23 22:50:13 -08:00
Leonardo de Moura
8d7bd34059 fix(doc/make/split-stack): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:45:13 -08:00
Leonardo de Moura
d06f4fa3d1 fix(doc/make/split-stack): typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:41:16 -08:00
Leonardo de Moura
0cd8e3e76b feat(split-stack): add support for split-stacks (no more stackoverflows) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 22:30:54 -08:00
Leonardo de Moura
29613e45ad doc(README.md): Boost support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:45:31 -08:00
Leonardo de Moura
1eeec07713 doc(lua): add options documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 11:02:34 -08:00