Gabriel Ebner
|
fcc559a7f0
|
feat(library/init/util): add trace_call_stack function
|
2017-01-12 21:47:46 +01: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
|
b8f1b16cfe
|
chore(init/meta/smt/congruence_closure): remove unnecessary line
|
2017-01-10 09:07:37 -08:00 |
|
Leonardo de Moura
|
a43b856086
|
feat(library/init/meta/smt): add simp tactics to smt_tactic
We can simplify the target without affecting the smt state
|
2017-01-09 19:19:48 -08:00 |
|
Leonardo de Moura
|
5050e40aec
|
feat(library/init/meta/smt): add slift smt tactic
|
2017-01-09 19:07:54 -08:00 |
|
Leonardo de Moura
|
b1c1d2dfa4
|
feat(library/init/meta): improve dsimp tactic notation
|
2017-01-09 17:31:35 -08:00 |
|
Leonardo de Moura
|
fa4d47edd8
|
chore(library/init/algebra/ring): document messy problem in the algebraic hierarchy
|
2017-01-08 23:35:39 -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
|
0c4c41ae54
|
feat(library/init/meta): produce nicer error message for overloaded simp/ematch lemma
|
2017-01-07 14:13:46 -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
|
d333c444cd
|
test(tests/lean/run): add tactic examples
|
2017-01-06 18:48:03 -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
|
13a11b4374
|
feat(library/init/meta/interactive): add get_eqn_lemmas_for tactic, allow user to provide definition name as an argument to simp
|
2017-01-06 11:45:09 -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 |
|
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
|
4a76579cd0
|
feat(library/tactic/smt): add tactics for getting/setting ematching lemmas
|
2017-01-05 20:35:57 -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
|
4d4e47921a
|
fix(library/init/core): mark all rfl-lemmas as lemmas
|
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
|
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
|
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
|
0969997c64
|
feat(library/tactic/smt): add ematch smt_tactic
|
2017-01-04 22:41:36 -08:00 |
|
Leonardo de Moura
|
858ce76e73
|
feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas
|
2017-01-04 20:31:38 -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
|
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 |
|
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
|
59f3c9775a
|
feat(frontends/lean/tactic_notation): add support for begin [smt] ... end blocks
TODO: add support for inspecting intermediate states.
|
2017-01-04 11:13:00 -08:00 |
|
Leonardo de Moura
|
3a62ca0581
|
refactor(library/init/meta): move smt tactics to library/init/meta/smt, and add interactive definitions
|
2017-01-04 09:36:50 -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
|
554cef1d36
|
feat(library/tactic/smt/congruence_closure): propagate disequalities
|
2017-01-03 14:53:27 -08:00 |
|
Leonardo de Moura
|
78f4ab605e
|
feat(library/tactic/smt): preprocessing configuration options
|
2017-01-03 11:06:33 -08:00 |
|
Leonardo de Moura
|
de8491474c
|
feat(library/tactic/smt/congruence_closure): more propagation rules for implication, and cleanup
|
2017-01-02 19:35:12 -08:00 |
|
Leonardo de Moura
|
cefccd0e47
|
feat(library/tactic/smt): perform "unit propagation" in the congruence closure module
|
2017-01-02 18:49:26 -08:00 |
|
Leonardo de Moura
|
b200a86240
|
feat(library/tactic/smt): simplify congruence_closure internalization, visit lemmas at unit_propagation
|
2017-01-02 12:23:32 -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
|
50b25ad45f
|
feat(library/init/meta/smt_tactic): add smt_tactic.destruct, and a few combinators
|
2017-01-01 14:50:34 -08:00 |
|
Leonardo de Moura
|
effe19d334
|
feat(library/tactic/smt/smt_state): add smt_tactic.intros, define smt_state in Lean as (list smt_goal)
|
2017-01-01 14:17:03 -08:00 |
|