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
|
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
|
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 |
|
Leonardo de Moura
|
62483b793f
|
feat(library/standard): add notation for symm, trans and subst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 22:49:12 -07:00 |
|
Leonardo de Moura
|
ebf34f2fe9
|
refactor(library/standard): mark 'not' as transparent
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 22:14:15 -07:00 |
|
Leonardo de Moura
|
d84a4bea5f
|
chore(library/standard): port (an older version of) Floris's nat library to Lean 0.2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 20:31:28 -07:00 |
|
Leonardo de Moura
|
fd0deb4555
|
feat(library/standard): add basic properties of binary functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 17:48:30 -07:00 |
|
Leonardo de Moura
|
bfdf187ce7
|
refactor(library/standard): rename rec to rec_on
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 17:01:51 -07:00 |
|
Leonardo de Moura
|
5529ef1056
|
feat(library/standard): add function 'helper' module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 16:29:39 -07:00 |
|
Leonardo de Moura
|
5296275c41
|
feat(library/standard/logic): add imp_or theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 12:29:23 -07:00 |
|
Leonardo de Moura
|
08174f904b
|
feat(library/standard/logic): mark 'not equal' as an abbreviation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-24 12:01:09 -07:00 |
|
Leonardo de Moura
|
8adf6e25ef
|
refactor(library/standard/unit): make unit type similar to the one in the hott library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 09:56:05 -07:00 |
|
Leonardo de Moura
|
c5cbe1cc2c
|
refactor(library/standard): rename bool_decidable to prop_decidable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 09:53:05 -07:00 |
|
Leonardo de Moura
|
b522ea6f2d
|
refactor(library/standard): rename bit to bool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 09:49:54 -07:00 |
|
Leonardo de Moura
|
5eaf04518b
|
refactor(*): rename Bool to Prop
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 09:43:18 -07:00 |
|
Leonardo de Moura
|
b7838f5db7
|
feat(library/standard/cast): add dcongr2 theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 05:58:58 -07:00 |
|
Leonardo de Moura
|
1e595e8027
|
feat(library/standard/decidable): decidable is proof irrelevant
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 03:54:28 -07:00 |
|
Leonardo de Moura
|
c0f862d88a
|
feat(library/standard): add Diaconescu's theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 21:15:48 -07:00 |
|
Leonardo de Moura
|
13804f75f9
|
feat(library/standard/logic): iff is refl, trans, and symm
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 21:10:30 -07:00 |
|
Leonardo de Moura
|
29b6d1081c
|
feat(library/standard/bool_decidable): cleanup bool_decidable, and remove the artificial dependency to bit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-21 02:42:11 +01:00 |
|
Leonardo de Moura
|
293ed333c7
|
feat(library/standard/if): cleanup 'if-then-else' theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-21 02:40:43 +01:00 |
|
Leonardo de Moura
|
5e8c128b00
|
feat(library/standard): add more decidable instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 01:10:49 +01:00 |
|
Leonardo de Moura
|
c37b5afe93
|
feat(library/standard): add decidable class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 00:19:32 +01:00 |
|
Leonardo de Moura
|
4a0e701f6d
|
feat(library/standard/bit): add theorems and notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 00:19:32 +01:00 |
|
Leonardo de Moura
|
8b70ffb0a4
|
feat(library/standard): add equivalence inductive predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-20 00:19:31 +01:00 |
|
Leonardo de Moura
|
e817260c6d
|
feat(library/standard): add or_comm, and_comm, ... theorems, cleanup notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-19 09:29:04 +01:00 |
|
Leonardo de Moura
|
f942c6f64c
|
feat(library/standard/classical): add Peirce's law
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 03:05:34 +01:00 |
|
Leonardo de Moura
|
e3f364e1ee
|
feat(library/standard): add well-founded induction theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 02:48:40 +01:00 |
|
Leonardo de Moura
|
638bdd5e12
|
feat(library/standard): add forall and exists theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 02:48:00 +01:00 |
|
Leonardo de Moura
|
9cb238534d
|
feat(library/standard): add hilbert's choice operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 01:39:35 +01:00 |
|
Leonardo de Moura
|
ea2fffc260
|
feat(library/standard): add inhabited_exists theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-13 00:24:58 +01:00 |
|
Leonardo de Moura
|
0bd943574e
|
fix(library/standard): make sure file can be compiled when processing theorems in parallel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 23:55:50 +01:00 |
|
Leonardo de Moura
|
ae2f019c23
|
refactor(library/standard): reorganize cast and piext theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 20:24:36 +01:00 |
|
Leonardo de Moura
|
bd82f5e81c
|
chore(library/standard/piext): cleanup hcongr proof
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 19:08:53 +01:00 |
|
Leonardo de Moura
|
319b1fb8d1
|
feat(library/standard): add piext axiom, and theorems that follow from it
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 09:44:46 +01:00 |
|
Leonardo de Moura
|
cd806bfabb
|
refactor(library/standard): move cast and heq to separate file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 07:08:12 +01:00 |
|
Leonardo de Moura
|
1d273fcfdd
|
chore(frontends/lean): rename 'obtains' to 'obtain'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 06:35:24 +01:00 |
|
Leonardo de Moura
|
24540056c5
|
feat(library/standard): add basic heq theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 06:21:00 +01:00 |
|