Leonardo de Moura
5b7d254e52
feat(builtin): add pre-compiled .lean builtin files to repository
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 11:49:17 -08:00
Leonardo de Moura
ba592c845c
fix(builtin): dependencies
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 11:19:17 -08:00
Leonardo de Moura
411ebbc3c1
refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file
...
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:04:49 -08:00
Leonardo de Moura
a05c815d31
chore(builtin): cleanup cmake file
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 22:27:36 -08:00
Leonardo de Moura
66178ae65a
refactor(extra): move extra to builtin
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 22:06:11 -08:00
