Leonardo de Moura
|
ff455d3ec9
|
chore(library/vm/vm): warning
|
2017-01-06 21:22:27 -08:00 |
|
Leonardo de Moura
|
8c652600dd
|
feat(library/tactic/smt/smt_state): ematch tactics fail if no instance is produced
The goal is to avoid nontermination of (repeat {ematch}) when the goal
is not provable. Of course, if there is a matching loop, it will still loop.
|
2017-01-06 21:20:01 -08:00 |
|
Leonardo de Moura
|
d81acfc44a
|
feat(library/tactic/smt/smt_state): use eta reduction in the smt preprocessor
|
2017-01-06 20:23:41 -08:00 |
|
Leonardo de Moura
|
c29a2bdac9
|
feat(library/init/meta/tactic): add eta reduction tactic
|
2017-01-06 19:56:10 -08:00 |
|
Leonardo de Moura
|
36453b894d
|
fix(library/print): avoid numerical internal names in the pretty printer
|
2017-01-06 19:27:31 -08:00 |
|
Leonardo de Moura
|
de8ba72a86
|
feat(library/vm/vm): suppress snapshots when printing profiling information
|
2017-01-06 19:22:07 -08:00 |
|
Leonardo de Moura
|
93c8e69313
|
chore(frontends/lean, library): cleanup anonymous instance management
|
2017-01-06 14:37:44 -08:00 |
|
Leonardo de Moura
|
b86aef1ff0
|
feat(shell/completion): do not show internal declarations
|
2017-01-06 14:14:43 -08:00 |
|
Leonardo de Moura
|
5e3f26ec95
|
feat(library/tactic/smt/congruence_closure): propagate not_exists
|
2017-01-06 14:00:36 -08:00 |
|
Leonardo de Moura
|
d5da18299b
|
feat(library/private): make sure the private prefix is an internal name
|
2017-01-06 11:48:05 -08:00 |
|
Leonardo de Moura
|
db70c78704
|
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
|
2017-01-06 11:40:34 -08:00 |
|
Gabriel Ebner
|
70e41305e5
|
fix(module_mgr): produce olean files with correct mtimes
|
2017-01-06 01:04:18 -08:00 |
|
Leonardo de Moura
|
15eaf30192
|
feat(library/tactic/smt/smt_state): allow user to provide a function ("to be unfolded") in the ematch_using tactic
|
2017-01-06 00:33:58 -08:00 |
|
Leonardo de Moura
|
7e4b79b221
|
feat(library/tactic/smt/smt_state): add ematch_using tactic
|
2017-01-06 00:24:25 -08:00 |
|
Leonardo de Moura
|
6f328071ff
|
feat(library/tactic/smt/congruence_closure): basic support for beta-reduction
|
2017-01-05 23:36:14 -08:00 |
|
Leonardo de Moura
|
0a2f7555b7
|
feat(library/tactic/smt/congruence_closure): improve pp_eqc
|
2017-01-05 20:46:36 -08:00 |
|
Leonardo de Moura
|
4a76579cd0
|
feat(library/tactic/smt): add tactics for getting/setting ematching lemmas
|
2017-01-05 20:35:57 -08:00 |
|
Leonardo de Moura
|
5723b63afe
|
feat(library/tactic/smt/smt_state): add new tracing for smt
|
2017-01-05 18:47:42 -08:00 |
|
Leonardo de Moura
|
7ba889b5cf
|
feat(frontends/lean/tactic_notation): try/repeat for smt_tactic in interactive mode
|
2017-01-05 18:31:57 -08:00 |
|
Gabriel Ebner
|
bc09a53f71
|
feat(library/task_queue): add flag to prevent priority inversion
|
2017-01-05 18:09:28 -08:00 |
|
Gabriel Ebner
|
063130ee18
|
feat(kernel/environment): add function that checks whether all proofs are correct
|
2017-01-05 18:09:28 -08:00 |
|
Leonardo de Moura
|
82f8eeb280
|
feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler
|
2017-01-05 18:02:14 -08:00 |
|
Leonardo de Moura
|
1395bebc44
|
feat(library/type_context): avoid typing errors due to reducibility when checking types at metavariable assignment
|
2017-01-05 18:01:23 -08:00 |
|
Leonardo de Moura
|
044fe965da
|
fix(library/tactic/unfold_tactic): failed to unfold prefix
|
2017-01-05 18:01:19 -08:00 |
|
Leonardo de Moura
|
b18b49dd6b
|
feat(library/tactic/smt/smt_state): add tactic for adding equational lemmas for a definition
|
2017-01-05 15:47:58 -08:00 |
|
Leonardo de Moura
|
3742d6573d
|
feat(library/tactic/smt/smt_state): add preprocess tactic
|
2017-01-05 13:43:50 -08:00 |
|
Leonardo de Moura
|
f008e623e9
|
feat(library/tactic/smt/smt_state): improve pretty printer for smt state
|
2017-01-05 13:12:15 -08:00 |
|
Leonardo de Moura
|
8eadaf51d8
|
feat(library/init/meta/smt): add helper tactics: get_facts, proof_for, refutation_for, add_lemmas_from_facts, ...
|
2017-01-05 12:59:11 -08:00 |
|
Leonardo de Moura
|
52c1a15313
|
feat(library/tactic/smt): add tactics for adding new lemmas to ematch state
|
2017-01-05 11:44:25 -08:00 |
|
Leonardo de Moura
|
b8e09bb86e
|
refactor(library/tactic/smt): move ematch Lean bindings to ematch.cpp
|
2017-01-05 10:35:59 -08:00 |
|
Leonardo de Moura
|
aaffcc59a9
|
refactor(library/tactic/smt): move hinst_lemma(s) Lean bindings to hinst_lemmas.cpp
|
2017-01-05 10:30:34 -08:00 |
|
Leonardo de Moura
|
0969997c64
|
feat(library/tactic/smt): add ematch smt_tactic
|
2017-01-04 22:41:36 -08:00 |
|
Leonardo de Moura
|
df9ee8be69
|
chore(library/tactic/smt/hinst_lemmas): style
|
2017-01-04 20:38:15 -08:00 |
|
Leonardo de Moura
|
d784aba249
|
feat(library/tactic/smt/hinst_lemmas): change how transparency is used to process hinst_lemmas
|
2017-01-04 19:12:37 -08:00 |
|
Leonardo de Moura
|
7c6f449db0
|
chore(library/tactic/smt/hinst_lemmas): improve error message
|
2017-01-04 18:15:15 -08:00 |
|
Leonardo de Moura
|
8144eaa9bf
|
feat(library/init/meta/smt/ematch): add hinst_lemmas API
|
2017-01-04 18:04:53 -08:00 |
|
Leonardo de Moura
|
384e8bc795
|
refactor(library/init/meta/smt): move ematch stuff to new file, and remove priority from hinst_lemma
|
2017-01-04 17:23:06 -08:00 |
|
Gabriel Ebner
|
9435762643
|
fix(compiler/vm_compiler): only compile computable non-builtin definitions
|
2017-01-04 16:30:22 -08:00 |
|
Gabriel Ebner
|
96398500b6
|
fix(library/module_mgr): do not cause waits for preimported modules
|
2017-01-04 16:30:22 -08:00 |
|
Gabriel Ebner
|
c9d2eeccf2
|
refactor(library/module): keep track of trust level in decl_modification
|
2017-01-04 16:30:22 -08:00 |
|
Gabriel Ebner
|
f6b8eb6821
|
feat(util/task_queue): lazy tasks
|
2017-01-04 16:30:22 -08:00 |
|
Leonardo de Moura
|
2e15304f05
|
feat(frontends/lean): add support for smt_state in the info_manager
|
2017-01-04 14:23:48 -08:00 |
|
Leonardo de Moura
|
5f2b247af9
|
feat(frontends/lean/tactic_evaluator): step-by-step evaluation for 'begin [smt] ... end' blocks
|
2017-01-04 14:06:44 -08:00 |
|
Leonardo de Moura
|
d53215a2fb
|
feat(frontends/lean/tactic_notation, library/init/meta/smt): add by_cases and by_contradiction smt_tactics, support for classical reasoning, add support for 'begin [smt] with config, ... end'
|
2017-01-04 12:03:45 -08:00 |
|
Leonardo de Moura
|
8a74a76720
|
chore(library/scope_pos_info_provider): style
|
2017-01-04 08:45:01 -08:00 |
|
Leonardo de Moura
|
d6ab3739ff
|
refactor(frontends/lean/elaborator): move tactic executation code to tactic_evaluator
|
2017-01-04 08:42:59 -08:00 |
|
Leonardo de Moura
|
0319fd5728
|
refactor(frontends/lean/elaborator): move pos_string_for
|
2017-01-04 07:32:44 -08:00 |
|
Leonardo de Moura
|
30d90533bc
|
feat(library/tactic/destruct_tactic): support for non-dependent elimination
|
2017-01-03 18:33:57 -08:00 |
|
Leonardo de Moura
|
3adcf30d2f
|
feat(library/init/meta/smt_tactic): add assert/assertv/define/definev/pose/note for smt_tactic
|
2017-01-03 17:12:00 -08:00 |
|
Leonardo de Moura
|
d546671849
|
chore(library/local_context): style
|
2017-01-03 15:00:46 -08:00 |
|