Gabriel Ebner
7ff2a77d67
feat(library/vm/vm_task): expose task_result objects to VM
2016-11-29 11:12:43 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
94c882f4d5
feat(library/documentation, frontends/lean): add /-! -/ doc string module block
2016-11-27 12:23:53 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
Leonardo de Moura
5daf1986e7
feat(library/init/nat): add nat.zero = zero (rfl) lemma
2016-11-26 10:54:28 -08:00
Leonardo de Moura
abc84452bc
fix(library/init/group): add group lemmas and use transport
2016-11-26 10:46:02 -08:00
Leonardo de Moura
338a46c225
fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map
2016-11-26 09:41:07 -08:00
Leonardo de Moura
ef34ab0148
feat(library/init): add lemmas for norm_num
2016-11-25 19:11:07 -08:00
Leonardo de Moura
4a31d541c9
feat(library/init/ring): add comm_ring, integral_domain
2016-11-25 18:53:03 -08:00
Leonardo de Moura
e9f8f9e5d7
refactor(library/nat): rename nat.le to nat.less_than
...
Motivation: avoid overload when we use `open nat`.
Unfortunately, we currently do not allow users to mark inductive datatype
declarations as protected.
2016-11-25 18:53:03 -08:00
Leonardo de Moura
efa760fc74
feat(library/init/nat_lemmas): add extra instances for short circuiting type class resolution
2016-11-25 18:53:03 -08:00
Leonardo de Moura
97dd2f34d5
feat(library,frontends/lean): add basic doc string support
2016-11-25 18:52:56 -08:00
Leonardo de Moura
4d36effe85
feat(library/init/ordered_ring): add linear_ordered_ring
2016-11-24 14:34:49 -08:00
Leonardo de Moura
baed136148
feat(library/init/ordered_ring): add ordered_ring -> ordered_semiring instance
2016-11-24 14:30:28 -08:00
Leonardo de Moura
2135d49957
feat(library/init/ordered_group): add more aux lemmas
2016-11-24 14:23:00 -08:00
Leonardo de Moura
25639f0b72
feat(library/init/meta): add 'pose' tactic
2016-11-24 13:48:16 -08:00
Leonardo de Moura
50f350f832
feat(library/init/ring): add ring -> semiring instance
2016-11-24 12:27:50 -08:00
Leonardo de Moura
0554fd5997
fix(frontends/lean): name resolution at tactic execution time
...
This commit also adds a new tactic: tactic.resolve_name
closes #1201
2016-11-24 10:55:39 -08:00
Leonardo de Moura
a4f491a3ad
feat(library/init/meta/interactive): add rename tactic to interactive mode
2016-11-24 09:54:55 -08:00
Leonardo de Moura
3b09865684
feat(library/init/meta/simp_tactic): add tactics for validating simp lemmas
2016-11-23 17:43:55 -08:00
Leonardo de Moura
21bad7cb97
feat(library/init/meta/comp_value_tactics): add support for char/string/fin at comp_val tactic
2016-11-23 13:19:54 -08:00
Leonardo de Moura
98fbe76f30
feat(library/comp_val): add mk_string_val_ne_proof
2016-11-23 13:19:24 -08:00
Leonardo de Moura
01bc4dfcd2
feat(library/init/meta/tactic): add dec_trivial notation
2016-11-23 11:42:57 -08:00
Leonardo de Moura
6f0d8cb258
refactor(library/init/string): do not mark string as reducible
2016-11-23 11:28:20 -08:00
Leonardo de Moura
11ef0b14fd
feat(library/data): add decidable_eq instances for bitvec and tuple
2016-11-23 11:09:24 -08:00
Leonardo de Moura
0d2d595c31
chore(library/init): remove unnecessary space
2016-11-23 10:53:19 -08:00
Leonardo de Moura
680bab8bb8
feat(library/comp_val): add mk_fin_val_ne_proof and mk_char_val_ne_proof
2016-11-23 10:25:04 -08:00
Leonardo de Moura
edaf03ae98
feat(library/init): add more lemmas and define ordered_ring
2016-11-22 20:50:21 -08:00
Leonardo de Moura
8966146a3d
fix(library/init): list of authors
2016-11-22 19:03:16 -08:00
Leonardo de Moura
242ad1bd65
feat(library/init/meta/comp_value_tactics): add comp_val tactic for testing
2016-11-22 17:03:21 -08:00
Leonardo de Moura
79000e9c50
fix(library/init/nat_lemmas): missing theorem used by comp_val.cpp
2016-11-22 16:59:31 -08:00
Leonardo de Moura
d3d10edbf0
fix(library/comp_val): missing case
2016-11-22 16:50:11 -08:00
Leonardo de Moura
f3e4c734fd
fix(library/init): instance priorities
2016-11-22 16:04:40 -08:00
Leonardo de Moura
207bc0ecad
feat(library/init/nat_lemmas): add lemmas for comparing nat values
2016-11-22 14:40:53 -08:00
Leonardo de Moura
c8f7dd384b
fix(library/init): implicit arguments
2016-11-22 14:40:03 -08:00
Leonardo de Moura
312689ec7f
feat(library/init/nat_lemmas): nat is a decidable_linear_ordered_semiring
2016-11-22 13:40:23 -08:00
Leonardo de Moura
e720ac929d
refactor(library/init): break algebra.lean in smaller pieces
2016-11-22 13:23:04 -08:00
Leonardo de Moura
362f972eda
feat(library/init/algebra): add ordered semiring structures
2016-11-22 12:58:05 -08:00
Leonardo de Moura
8352f36891
feat(library/init/algebra): more ordered structures
2016-11-22 12:34:31 -08:00
Leonardo de Moura
f253415c33
feat(library/init/algebra): add ordered_cancel_comm_monoid
2016-11-22 11:37:53 -08:00
Leonardo de Moura
1ebe2b590d
feat(library/data/bitvec): define has_one for (bitvec 0) too.
2016-11-22 10:42:13 -08:00
Leonardo de Moura
b35aef2895
feat(library/data/bitvec): add has_to_string instance
2016-11-22 10:36:45 -08:00
Leonardo de Moura
b56a9fba34
feat(library/init/nat_lemmas): add instance comm_semiring nat
2016-11-22 09:27:53 -08:00
Leonardo de Moura
43c1913747
chore(library/init/nat_lemmas): add simple theorems
2016-11-22 09:00:47 -08:00
Leonardo de Moura
9a932fa654
feat(library/init/algebra): define semiring and ring structures
2016-11-22 08:51:34 -08:00
Leonardo de Moura
2725383963
chore(library/init/algebra): use more general transport from library_dev
2016-11-22 08:41:25 -08:00
Leonardo de Moura
ac4cd3d733
feat(library/tactic/rewrite_tactic): disable pp.beta at rewrite error msg
2016-11-21 15:58:11 -08:00
Leonardo de Moura
9d52b6607d
feat(library/tactic): use annotated_head_beta_reduce instead of head_beta_reduce in tactics
2016-11-21 15:40:12 -08:00
Daniel Selsam
19596eae77
fix(library/init/logic.lean): if_true and if_false take instance as implicit instead of inst_implicit
2016-11-21 12:27:40 -08:00
Leonardo de Moura
a8267a8e41
feat(library/init/nat_lemmas): add more lemmas needed by basic automation
2016-11-21 12:18:28 -08:00
