Leonardo de Moura aac7777beb perf(library/tactic/unfold_tactic): implement dunfold_core and dunfold_occs_core in C++ ... Before this commit they were implemented using C++ and Lean. A Lean procedure was being invoked for each subterm of the input term. This is one of the performance problems at issue #1646. Here are the runtimes for size 7 in the example described at issue #1646. Before this commit: tactic execution took 7.48s elaboration of some_lifted_lets took 11.5s type checking time of some_lifted_lets took 33.4ms (aka QED time) total execution time: 16.841s After this commit: tactic execution took 4.96s elaboration of some_lifted_lets took 7.6s type checking time of some_lifted_lets took 31.1ms (aka QED time) total execution time: 12.785s		2017-06-06 14:35:05 -07:00
..
algebra	feat(init/data/int,init/data/nat,init/algebra): more algebra theorems	2017-06-01 15:15:40 -07:00
category	chore(init/category/monad): proof optimization	2017-05-27 04:14:04 -04:00
data	fix(library/init/meta/interactive): use replace_target at simp_goal	2017-06-05 15:21:20 -07:00
meta	perf(library/tactic/unfold_tactic): implement dunfold_core and dunfold_occs_core in C++	2017-06-06 14:35:05 -07:00
native	refactor(init): use list for expr.macro args	2017-05-14 19:17:28 -07:00
.gdb_history	chore(library, tests): switch to new attribute declaration syntax	2016-08-12 15:36:12 -07:00
cc_lemmas.lean	feat(frontends/lean): use . for field access	2017-03-28 15:29:54 -07:00
classical.lean	fix(library/noncomputable): fixes #1631	2017-05-31 23:16:37 -07:00
coe.lean	feat(library/data/list, library/data/array): theorems needed for new hash_map	2017-05-16 14:38:43 -07:00
core.lean	feat(library/init): heterogeneous andthen type class, and tactic.seq_focus implementation	2017-06-02 10:38:27 -07:00
default.lean	feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs	2017-05-23 22:07:46 -07:00
function.lean	chore(library/init): remove reducible annotations for id, const, etc, and move $ notation to core.lean	2017-03-11 11:34:16 -08:00
funext.lean	refactor(init/funext): shorten proof	2017-05-27 04:13:59 -04:00
init.md	chore(*.md): fix/remove broken links	2016-02-23 10:11:24 -08:00
logic.lean	chore(init/logic): slightly more efficient decidability of iff, xor	2017-05-27 04:16:25 -04:00
propext.lean	feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term	2017-03-28 17:47:49 -07:00
relator.lean	feat(init/relator): some new base theorems for transfer tactic	2017-05-27 04:16:25 -04:00
util.lean	refactor(init): replace has_quote class with reflected	2017-05-09 16:02:42 -07:00
wf.lean	feat(library/init): use Sort instead of Type for defining acc and well_founded	2017-05-23 16:40:45 -07:00