Soonho Kong
|
76d310da8b
|
chore(library/.gitignore): add TAGS
|
2014-08-15 20:55:38 -07:00 |
|
Soonho Kong
|
009e9fb3e6
|
feat(library/Makefile.common): add tags target
|
2014-08-15 20:52:29 -07:00 |
|
Leonardo de Moura
|
670bfe24f5
|
chore(build): remove hott library directory, and move hott tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-15 13:30:56 -07:00 |
|
Jeremy Avigad
|
5b7fb1f61a
|
feat(library/standard/classes): add nonempty
|
2014-08-15 13:06:27 -07:00 |
|
Jeremy Avigad
|
39c1683546
|
feat(library/standard/logic): add class nonempty
|
2014-08-15 12:58:58 -07:00 |
|
Jeremy Avigad
|
2d69303344
|
feat(library/standard): add sigma types and subtypes, make inhabited constructive
|
2014-08-15 12:58:58 -07:00 |
|
Jeremy Avigad
|
a1645c5ce5
|
feat(library/standard/hott/path.lean): add theorems and clean up file
|
2014-08-15 12:58:58 -07:00 |
|
Jeremy Avigad
|
7d7655c3f1
|
refactor(library/standard): integrate hott with standard library
|
2014-08-15 12:58:58 -07:00 |
|
Jeremy Avigad
|
218c9dfc81
|
feat(library/hott): begin porting Coq HoTT
|
2014-08-15 12:58:58 -07:00 |
|
Jeremy Avigad
|
0ea2d287e1
|
feat(library/standard): add classes for relations
|
2014-08-15 12:58:58 -07:00 |
|
Soonho Kong
|
caa47b9a70
|
fix(library): add LEAN_VERSION_FILE to Makefile.common
|
2014-08-14 18:21:58 -07:00 |
|
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 |
|