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

141 commits

Author SHA1 Message Date
Leonardo de Moura
2225a2acc5 feat(library/Makefile.common): generate .ilean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 18:05:48 -07:00
Leonardo de Moura
e1c97d1fc4 fix(library): remove LEAN_VERSION_FILE from Makefile.common, it breaks the build on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 18:05:48 -07:00
Soonho Kong
6f2c14be23 feat(library/Makefile.common): add dependency on bin/version 
This is related with issue #43.

[skip ci]
 2014-08-14 15:46:13 -07:00
Soonho Kong
87632622ee chore(library): add .gitignore 
[skip ci]
 2014-08-14 15:31:57 -07:00
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
f319d084d4 feat(library/Makefile.common): use new --cache/-c option at Makefile.common 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 11:20:08 -07:00
Leonardo de Moura
f6ba6da4b5 fix(library/standard): add missing 'end' of namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 17:52:51 -07:00
Leonardo de Moura
1a67e69678 feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:59:08 -07:00
Soonho Kong
e0bc5915fb fix(library/standard): remove long comments introduced by b2c2d1d 2014-08-07 11:59:59 -07:00
Soonho Kong
8d4c7b4b2c fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott" 2014-08-07 09:59:15 -07:00
Leonardo de Moura
59f6cb5962 fix(build): delete incorrect/old .d and .olean files, detect errors when generating .d files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:48 -07:00
Leonardo de Moura
d5bb7d45ec fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Leonardo de Moura
47d49643b0 feat(library/standard/logic/connectives/if): add more general if_congr theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Soonho Kong
d8ae285f93 fix(library/Makefile.common): clean remove olean/d files recursively 
[skip ci]
 2014-08-04 11:47:24 -07:00
Leonardo de Moura
94efd51fc5 chore(library/standard/logic/connectives/if): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 23:11:52 -07:00
Leonardo de Moura
c3f57cdb1c feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 22:58:12 -07:00
Leonardo de Moura
ae2e0fd3dc feat(library/standard/logic/connectives/if): add 'if-then-else' congruence theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 21:41:01 -07:00
Leonardo de Moura
f3cb5f2f84 feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 20:03:49 -07:00
Leonardo de Moura
aeebd942f2 refactor(library/standard): use relative paths in some files in the standard library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 20:04:27 -07:00
Leonardo de Moura
4b030c5d5f feat(library/module): relative module path 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 19:47:55 -07:00
Leonardo de Moura
700c911cf7 chore(library/standard/logic/class/decidable): add missing 'end' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 17:00:01 -07:00
Leonardo de Moura
148836d14b feat(library/standard/data/option): add basic theorems for option types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 16:59:01 -07:00
Jeremy Avigad
b832b2e33e refactor(library/standard/data/nat): stylistic changes 2014-08-01 21:22:54 -07:00
Jeremy Avigad
b5db9a4797 feat(library/standard/data/nat): port most recent nat to lean 0.2 2014-08-01 21:22:53 -07:00
Jeremy Avigad
4b05e70762 feat(library/standard/logic/axioms): add import default 2014-08-01 21:22:53 -07:00
Jeremy Avigad
77931f2af8 feat(library/standard): add markdown documentation 2014-08-01 21:22:53 -07:00
Soonho Kong
3cb9b4c265 fix(library/Makefile.common): make OSX-compatible 2014-08-01 10:21:40 -07:00
Leonardo de Moura
d27c85e30c fix(library/Makefile.common): avoid error message when .d files do not exist 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:11:01 -07:00
Leonardo de Moura
f75beb8087 fix(library/standard/data/list/basic): remove 'sorry' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:15:30 -07:00
Jeremy Avigad
b2c2d1dd44 refactor(library/standard): organize files into a hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
fbaf8b7e77 refactor(library/standard): begin reorganization into hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
df84c4c2ca refactor(library/standard): clean up logic, reorder arguments to elim rules 2014-08-01 09:11:51 -07:00
Jeremy Avigad
c89c96b913 feat(library/standard/list.lean): add facts about lists 2014-08-01 09:11:51 -07:00
Jeremy Avigad
e846c8c76b index on master: 9dc1baa feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
5847743573 feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
8ea5dad4c0 feat(library/standard/congruence.lean): add class to infer that a function is a congruence with respect to two relations 2014-08-01 09:11:51 -07:00
Jeremy Avigad
09d5d074ec feat(library/standard/list.lean): begin to port lists from lean 0.1 2014-08-01 09:11:51 -07:00
Leonardo de Moura
b279c94037 feat(build): cread .d (dependency) files for .lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:08:16 -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
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
Leonardo de Moura
864fdd37da refactor(library/aliases): aliases are from name to names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 21:01:59 -07:00
Leonardo de Moura
5555d620cf feat(library/standard): add or_inl and or_inr as short-hands for the commonly used 'or_intro_left _' and 'or_intro_right _' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 17:25:57 -07:00
Leonardo de Moura
99a1966fd6 refactor(library/standard/set): use the same style for mem_inter and mem_union 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:32:59 -07:00
Leonardo de Moura
88130f339e feat(library/standard): add basic set theory that does not rely on classical axioms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:18:33 -07:00
Leonardo de Moura
3a77226b92 feat(library/standard/bool): add bor_to_or theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:17:55 -07:00
Leonardo de Moura
25f7929ea3 feat(library/standard/bool): add band_assoc and bor_assoc theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:50:57 -07:00
Leonardo de Moura
d9ee994281 feat(library/hott): copy basic files to hott library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:13:04 -07:00
Leonardo de Moura
abe1dbd7e0 refactor(library/standard): cleanup notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:36:28 -07:00
Leonardo de Moura
a450ad5a95 feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:24:01 -07:00
Leonardo de Moura
a5b9a7b296 fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:10:45 -07:00