Floris van Doorn
|
883b4fedb9
|
feat(hott): start with proof to characterize (is_trunc n A) using iterated loop spaces
|
2015-06-04 20:14:12 -04:00 |
|
Floris van Doorn
|
4117455e97
|
feat(hott): redefine nat.le and nat.lt
also some minor modifications in other files
|
2015-06-04 20:14:12 -04:00 |
|
Floris van Doorn
|
d4a991ef84
|
feat(hott): define cubes and cubeovers
|
2015-06-04 20:13:53 -04:00 |
|
Leonardo de Moura
|
63f61a35f4
|
feat(library/data/list/set): cleanup nodup_map proof
|
2015-06-04 15:21:40 -07:00 |
|
Leonardo de Moura
|
9a7cff0e89
|
feat(library/data/list/comb): add length_product theorem
|
2015-06-04 15:11:09 -07:00 |
|
Jeremy Avigad
|
df69bb4cfc
|
feat(library/*): add theorems from Haitao on sets and functions, clean up
|
2015-06-04 11:55:25 -07:00 |
|
Jeremy Avigad
|
03952ae12c
|
feat(library/logic/{connectives,identities},library/algebra/function): cleanup and some additions from Haitao Zhang
|
2015-06-04 11:55:25 -07:00 |
|
Leonardo de Moura
|
134740182d
|
fix(frontends/lean): fixes #652
|
2015-06-03 21:53:51 -07:00 |
|
Leonardo de Moura
|
c8ad1874a2
|
fix(library/util): compilation error in debug mode
|
2015-06-03 17:39:03 -07:00 |
|
Leonardo de Moura
|
68688ecdf6
|
fix(library/tactic/subst_tactic): in the standard mode, use dependent elimination in the subst tactic (when needed)
Before this commit, the subst tactic was producing an type incorrect
result when dependent elimination was needed (see new test for an example).
|
2015-06-03 17:36:04 -07:00 |
|
Leonardo de Moura
|
dce86b3a84
|
feat(library/init/logic): add 'eq.drec' (in standard Lean) with a signature very similar to eq.rec in the HoTT library
|
2015-06-03 17:29:26 -07:00 |
|
Leonardo de Moura
|
c841e63649
|
refactor(library/data/fintype): create 'fintype' subdirectory
|
2015-06-03 16:43:55 -07:00 |
|
Leonardo de Moura
|
2a6ea2c6fb
|
feat(library/data/finset/to_set): add to_set.inj
|
2015-06-03 14:05:43 -07:00 |
|
Leonardo de Moura
|
16d03c17ee
|
refactor(library/logic/eq): use 'substvars' tactic
|
2015-06-02 23:55:51 -07:00 |
|
Leonardo de Moura
|
a8c9121d2e
|
feat(library/data/vec): add vector as list subtype
|
2015-06-02 22:09:23 -07:00 |
|
Leonardo de Moura
|
7a39d5aaa3
|
feat(library/data): add auxiliary definitions
|
2015-06-02 22:08:25 -07:00 |
|
Leonardo de Moura
|
228a99af7e
|
feat(library/data/subtype): cleanup proof
|
2015-06-02 19:51:28 -07:00 |
|
Leonardo de Moura
|
70d0dea02d
|
feat(library/init/logic): add more congruence theorems
Remark: the simplifier should be able to select the "right" one.
|
2015-06-02 14:06:15 -07:00 |
|
Leonardo de Moura
|
2f9005827c
|
feat(library/init/logic): 'if-then-else' and 'dependent-if-then-else' congruence theorems
We will use these theorems to test the new simplifier.
|
2015-06-02 13:27:50 -07:00 |
|
Leonardo de Moura
|
50fe4ec6c0
|
feat(library/data/encodable): add quot.rep definition for choosing equivalence class representative for equivalence classes of encodable types
|
2015-06-02 11:03:24 -07:00 |
|
Leonardo de Moura
|
e7448ca77e
|
feat(library/init/quot): add exists_rep theorem for quotients
|
2015-06-02 10:52:07 -07:00 |
|
Leonardo de Moura
|
1ea56038e3
|
feat(library/init/quot): add has_decidable_eq definition for quotients
|
2015-06-02 10:47:20 -07:00 |
|
Leonardo de Moura
|
cfb102cbd1
|
fix(emacs/lean-mode): disable electric-indent-mode
closes #636
|
2015-06-01 22:42:57 -07:00 |
|
Leonardo de Moura
|
b2f8d2000c
|
fix(library/simplifier/rewrite_rule_set): avoid compiler specific behavior
|
2015-06-01 22:23:34 -07:00 |
|
Leonardo de Moura
|
d6997300f1
|
fix(library/private): use environment fingerprint to compute private decls "unique" identifier
fixes #648
|
2015-06-01 22:21:31 -07:00 |
|
Leonardo de Moura
|
4ace996057
|
fix(library/simplifier): bug in is_permutation_ceqv
|
2015-06-01 18:07:31 -07:00 |
|
Leonardo de Moura
|
0fbc944cdd
|
feat(frontends/lean): add '[rewrite]' attribute
|
2015-06-01 17:58:24 -07:00 |
|
Leonardo de Moura
|
d547698a56
|
refactor(library,library/tactic): move class_instance_synth to library
This module will be needed by the simplifier
|
2015-06-01 16:30:40 -07:00 |
|
Leonardo de Moura
|
8a89588079
|
refactor(library,library/tactic): move auxiliary procedures from tactic to library
|
2015-06-01 16:19:55 -07:00 |
|
Leonardo de Moura
|
9fc7bc6d25
|
chore(README): remove coverity link
|
2015-06-01 15:50:09 -07:00 |
|
Leonardo de Moura
|
b6fde68012
|
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples"
|
2015-06-01 15:35:28 -07:00 |
|
Leonardo de Moura
|
b62e6bb133
|
feat(library/simplifier): add rewrite rule sets
|
2015-06-01 15:15:57 -07:00 |
|
Leonardo de Moura
|
780d313686
|
fix(library/annotation): add missing == and hash methods for annotation class
We have multiple annotations. The default == and hash methods were
ignoring that.
|
2015-06-01 11:27:46 -07:00 |
|
Rob Lewis
|
b1404c5943
|
feat(library/data/real): fill in sorrys in proof that R is l.o. field
|
2015-06-01 23:00:53 +10:00 |
|
Rob Lewis
|
9843e61583
|
feat(library/data/real): define inverses of reals, prove (classically) that R is a discrete linear ordered field
|
2015-06-01 23:00:53 +10:00 |
|
Jeremy Avigad
|
fabdae6d54
|
refactor(hott/algebra/ring.lean,ordered_ring.lean): rename some theorems
|
2015-06-01 12:35:44 +10:00 |
|
Jeremy Avigad
|
82142b60f0
|
refactor(library/data/finset/basic.lean): remove finset / finset.finset duplicate
|
2015-06-01 12:35:44 +10:00 |
|
Jeremy Avigad
|
dcae29a253
|
feat(library/data/int/gcd.lean): add gcd for the integers
|
2015-06-01 12:35:44 +10:00 |
|
Jeremy Avigad
|
ffa648a090
|
feat/refactor(library/*): various additions and improvements
|
2015-06-01 12:35:44 +10:00 |
|
Jeremy Avigad
|
cdecc309b3
|
fix(library/data/finset/to_set.lean): to_set does not require decidable equality
|
2015-06-01 12:35:44 +10:00 |
|
Leonardo de Moura
|
1238f43575
|
feat(library/logic/examples): add "double-negation translation" example
|
2015-05-31 18:18:10 -07:00 |
|
Leonardo de Moura
|
55608c9b9f
|
fix(frontends/lean/pp): bug in pp arrow
|
2015-05-31 17:21:37 -07:00 |
|
Leonardo de Moura
|
ca110012d8
|
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
closes #645
|
2015-05-30 21:57:28 -07:00 |
|
Leonardo de Moura
|
e5a82ef516
|
feat(frontends/lean): add option for disabling "coercion lifting"
|
2015-05-30 17:07:42 -07:00 |
|
Leonardo de Moura
|
6f6848968d
|
feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case
closes #252
|
2015-05-30 16:44:26 -07:00 |
|
Leonardo de Moura
|
ea9c810fca
|
feat(frontends/lean/coercion_elaborator): implement "coercion lifting"
closes #644
|
2015-05-30 14:45:14 -07:00 |
|
Jeremy Avigad
|
b76445df39
|
feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int
|
2015-05-30 22:10:21 +10:00 |
|
Jeremy Avigad
|
c986ee305b
|
refactor(library/data/nat/gcd.lean): move gcd to a new file
|
2015-05-30 22:10:21 +10:00 |
|
Jeremy Avigad
|
cc0a620db1
|
feat(library/data/{nat,int}/div.lean): add to and improve div library
|
2015-05-30 22:10:21 +10:00 |
|
Leonardo de Moura
|
6d2f37857d
|
feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands
|
2015-05-29 16:47:29 -07:00 |
|