Leonardo de Moura
d0c86f13bb
chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob
2017-01-11 17:47:49 -08:00
Leonardo de Moura
f56250d41e
chore(library/init/data/nat/lemmas): mark nat.add_zero as protected
2017-01-07 14:17:56 -08:00
Leonardo de Moura
32cc36214a
feat(library/init/meta/smt_tactic): allow user to select simp attribute to be used during SMT preprocessing, use preprocessing at intros too
2017-01-01 22:26:26 -08:00
Leonardo de Moura
244e115412
chore(library/init/data): add more "short-circuit" instances for int/nat
2016-12-27 11:51:42 -08:00
Leonardo de Moura
58ca9a3059
feat(library/init/data/int/comp_lemmas): add auxiliary lemmas for comparing int numerals
2016-12-24 13:52:48 -08:00
Sebastian Ullrich
d95e817a56
refactor(library/data/{bitvec,tuple}): style, conventions, conversions
2016-12-18 13:25:00 -08:00
Leonardo de Moura
1726d37d4e
fix(library/algebra/order): decidable_linear_order
...
Add fields for decidable_eq and decidable_le.
We need this because a concrete instance may have its own
implementation that is not definitionally equal to
the old ones defined at library/algebra/order.lean.
Without this change, types such as nat and int would
have multiple definitions for decidable_eq and decidable_le
which are not definitionally equal.
2016-12-17 14:01:43 -08:00
Leonardo de Moura
422d43cf47
fix(library/init/data/nat/basic): issue reported by @kha
2016-12-17 13:17:30 -08:00
Jeremy Avigad
57dcbcc1c6
feat(library/init/data/nat/lemmas): add facts about order and subtraction
2016-12-15 09:56:09 -08:00
Leonardo de Moura
13ae8b07b3
feat(library/init/data/nat/lemmas): add missing lemmas
2016-12-12 13:25:30 -08:00
Leonardo de Moura
c8d6836aa1
feat(library): port nat sub lemmas
2016-12-11 09:46:45 -08:00
Leonardo de Moura
692701c5ef
feat(library/init/meta): use cheap "reflexivity" after simp and rewrite
...
The idea is to make sure lean doesn't timeout (at reflexivity) when we apply simp or
rewrite in goals such as
(x y : nat) |- x + y + 10000000000 = x + y + 200000000000000
This commit also addresses an issue raised at #1218
2016-12-08 14:41:26 -08:00
Jeremy Avigad
281903edee
refactor(library/init/data/nat/lemmas): better name for self_lt_succ
2016-12-08 07:20:39 -08:00
Jeremy Avigad
814da88858
refactor(library/init/data/nat/basic,lemmas): alternative name, and rename le.elim to le.dest
2016-12-08 07:20:02 -08:00
Leonardo de Moura
e423588463
refactor(library/init): merge some files
2016-12-02 16:13:45 -08:00
Leonardo de Moura
d96fed26b0
refactor(library/init): move propext to its own file
2016-12-02 16:04:39 -08:00
Leonardo de Moura
e11fd8820a
refactor(library/init): create init.data folder
2016-12-02 14:23:06 -08:00
