Leonardo de Moura
e8e483534b
chore(library/init/meta/decl_cmds): remove unused parameter
2017-01-18 19:44:16 -08:00
Leonardo de Moura
0795acaf6a
refactor(library/init/algebra): new transport from multiplicative to additive
...
The motivation is to avoid the problems produced by the "declare as
structure and then tag as class idiom" described in the file ring.lean.
2017-01-18 19:39:53 -08:00
Leonardo de Moura
d0a578c3db
feat(library/init/meta/environment): add is_projection
2017-01-18 18:12:08 -08:00
Leonardo de Moura
0ad053f0f1
feat(library/init/meta/decl_cmds): add command for copying type and value using replacement
2017-01-18 17:52:11 -08:00
Leonardo de Moura
694e6f47dc
fix(library/init/meta/smt/ematch,library/tactic/simp_lemmas): trick for adding equations of a definition to a simp/hinst lemma set
...
Before this commit, if we declared an equational lemma using 'def',
then it would not be correctly added to the simp/hinst lemma set.
The new test exposes the problem.
2017-01-18 02:05:04 -08:00
Leonardo de Moura
97b98c58d0
refactor(library): move nat lemmas to library/init/data/nat/lemmas.lean
2017-01-17 17:42:13 -08:00
Joe Hendrix
767ac42dfe
chore(library/data): remove redundent decidable_eq instances
2017-01-17 17:34:10 -08:00
Joe Hendrix
5bc5013f16
chore(library/data/bitvec): remove leftover code
2017-01-17 17:34:05 -08:00
Joe Hendrix
985c3697b9
chore(library/data/list): add back copyright notice
2017-01-17 17:33:59 -08:00
Joe Hendrix
24fc68cef4
feat(library/init/category/combinators.lean): add foldl and when
2017-01-17 17:33:50 -08:00
Joe Hendrix
8e2cf491e5
refactor(library/data/list): move theorems to separate modules per lean2
2017-01-17 17:33:45 -08:00
Joe Hendrix
3de9e722e1
feat(library/data/bitvec): additional definitions
2017-01-17 17:33:37 -08:00
Joe Hendrix
d52c3327ba
feat(library/data/nat/sub): additional theorems
2017-01-17 17:33:32 -08:00
Joe Hendrix
f244c0e70a
feat(library/data/bitvec): add bitvec version of tuple.append
2017-01-17 17:33:24 -08:00
Joe Hendrix
de92ea658a
feat(library/data/tuple): add decidable_eq to tuple
2017-01-17 17:33:17 -08:00
Joe Hendrix
9781a0414c
feat(library/data/list): add has_decidable_eq to list.
2017-01-17 17:33:09 -08:00
Joe Hendrix
18cbc22791
refactor(library/data/nat): migrate data.nat to lean2 structure
2017-01-17 17:24:37 -08:00
Leonardo de Moura
8e76d079d3
chore(tests/lean/run): fix tests
2017-01-17 15:50:54 -08:00
Leonardo de Moura
6ebc23eca4
feat(library/init/meta/smt/smt_tactic): add smt_tactic.induction
...
Non-interactive version.
2017-01-13 16:49:54 -08:00
Leonardo de Moura
05d86e49ca
feat(library/init/meta/smt): add intros variants for smt_tactic
2017-01-13 16:13:37 -08:00
François G. Dorais
b305130ec3
fix(library/init/wf): typo
...
Same typo as #1091 , different location.
2017-01-13 11:35:52 -08:00
Leonardo de Moura
69fd35f068
feat(library/init/meta/smt): add helper tactics and doc-strings
2017-01-13 11:21:20 -08:00
Leonardo de Moura
04fb7b88e7
feat(library/init/algebra): mark basic facts as [ematch] until we have support for arithmetic
2017-01-13 10:36:08 -08:00
Leonardo de Moura
6f4bcbab20
feat(library/init/meta/smt/ematch): convenient way of marking all equational lemmas of a giving definition as ematch lemmas
2017-01-13 10:35:09 -08:00
Leonardo de Moura
6588b04fd5
feat(library/init/meta/declaration): add helper definition for demos
2017-01-12 21:12:44 -08:00
Leonardo de Moura
d2e393c779
feat(library/init/logic): allow exists.intro to be used in pattern matching
2017-01-12 16:03:01 -08:00
Gabriel Ebner
51924eb726
refactor(tools/super/lpo): add mk_lpo function
2017-01-12 21:47:46 +01:00
Gabriel Ebner
f8caacfcb3
fix(tools/super/superposition): use none transparency to remove beta-redex
2017-01-12 21:47:46 +01:00
Gabriel Ebner
b6a25f8074
feat(tools/super/defs): unfold definitions using dunfold_expr_core
2017-01-12 21:47:46 +01:00
Gabriel Ebner
17bc32e41b
chore(tools/super/prover_state): clean up prover monad definition
2017-01-12 21:47:46 +01:00
Gabriel Ebner
020cb5b271
fix(tools/super/clause): fix universal closure of clauses with dependent types
2017-01-12 21:47:46 +01:00
Gabriel Ebner
8319a4c927
perf(tools/super/trim): make trim much cheaper
2017-01-12 21:47:46 +01:00
Gabriel Ebner
f2b3c7ae30
fix(tools/super/misc_preprocessing): normalize clauses during preprocessing
2017-01-12 21:47:46 +01:00
Gabriel Ebner
fcc559a7f0
feat(library/init/util): add trace_call_stack function
2017-01-12 21:47:46 +01:00
Gabriel Ebner
42eb3ef497
feat(tools/super/inhabited): look in the local context as well
2017-01-12 21:47:46 +01:00
Leonardo de Moura
3967cd28fa
fix(library/vm/vm): curr_fn() may not be available
2017-01-12 11:47:45 -08:00
Leonardo de Moura
df91ae3738
fix(library/string,library/init/data/to_string): handle ASCII control characters
2017-01-11 23:44:33 -08:00
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
d5c3736609
feat(library/init/meta/tactic): add helper tactic
2017-01-11 17:08:03 -08:00
Leonardo de Moura
5d3ac31f25
feat(library/init/data/list/lemmas): add lemmas for POPL demo
2017-01-11 17:07:37 -08:00
Leonardo de Moura
dc7e39887b
refactor(library/tools/super/simp): reorganize simplify lemmas API
2017-01-11 13:47:49 -08:00
Leonardo de Moura
178be8d8ea
fix(library/init/coe): coe should be reducible
2017-01-10 20:14:28 -08:00
Leonardo de Moura
e256022746
chore(library/init/meta/tactic): avoid the weird 'command' type when auto completing tactics
2017-01-10 14:59:10 -08:00
Leonardo de Moura
e96bbaee3f
fix(library/type_context): fix #1295
2017-01-10 11:54:38 -08:00
Jeremy Avigad
20edc93b17
fix(library/init/data/list/lemmas): fix theorem names, now nil_append and cons_append
2017-01-10 09:10:33 -08:00
Gabriel Ebner
d6a70b4aa3
chore(library/tools/super/clause_ops): remove unnecessary type annotations
2017-01-10 09:07:37 -08:00
Gabriel Ebner
890ba702e6
feat(tools/super/demod): demodulation
2017-01-10 09:07:37 -08:00
Gabriel Ebner
b8f1b16cfe
chore(init/meta/smt/congruence_closure): remove unnecessary line
2017-01-10 09:07:37 -08:00
Gabriel Ebner
e0dd8326c8
feat(tools/super/clause): more compact formatting
2017-01-10 09:07:37 -08:00
Gabriel Ebner
beb355f798
feat(tools/super): clausify during preprocessing
...
Some inference produce terms with large useless redexes such as
(prod.fst (prod.mk _ _)). Since we do normalization during
preprocessing, we can avoid ever even looking at these terms.
2017-01-10 09:07:37 -08:00
