Leonardo de Moura
|
7f1800962a
|
feat(frontends/lean/pp): allow user to override pp.all setting
see #922
|
2015-12-11 10:40:48 -08:00 |
|
Leonardo de Moura
|
0acdcd487b
|
feat(frontends/lean): add 'print aliases' command
|
2015-12-09 10:39:40 -08:00 |
|
Leonardo de Moura
|
34b944a71e
|
refactor(frontends/lean): remove broken 'migrate' command
|
2015-12-08 15:40:49 -08:00 |
|
Leonardo de Moura
|
7da64a768f
|
refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state
|
2015-12-08 14:58:08 -08:00 |
|
Leonardo de Moura
|
50df6b5698
|
feat(frontends/lean): rename '[intro]' ==> '[intro!]' and '[backward]' ==> '[intro]'
|
2015-12-07 21:33:35 -08:00 |
|
Leonardo de Moura
|
295b1d21f5
|
feat(frontends/lean): add '[intro]' and '[elim]' annotations
|
2015-12-07 18:43:15 -08:00 |
|
Leonardo de Moura
|
c3b5ce0785
|
feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns
|
2015-12-07 12:39:51 -08:00 |
|
Daniel Selsam
|
a9aeb69789
|
feat(frontends/lean/builtin_cmds): print metas for patterns
|
2015-12-07 12:32:22 -08:00 |
|
Daniel Selsam
|
25a3cff54e
|
refactor(library/abstract_expr_manager): remove fun_info_manager
|
2015-12-04 08:31:38 -08:00 |
|
Daniel Selsam
|
7854158751
|
fix(library/abstract_expr_manager): only squash Cast subsingletons
|
2015-12-04 08:31:38 -08:00 |
|
Daniel Selsam
|
139536896c
|
feat(library/light_lt_manager): light wrappers for ordered rewriting
|
2015-12-02 22:56:54 -08:00 |
|
Leonardo de Moura
|
028ef47c84
|
feat(frontends/lean,library/blast/forward/pattern): check whether patterns can be inferred at declaration time
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
f84c6a6cfa
|
fix(library/blast,frontends/lean): handling pattern hints after unfolding
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
950f356d9a
|
refactor(library/blast,frontends/lean): forward pattern index
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
4129b398da
|
fix(frontends/lean/builtin_cmds): private constants in the print command
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
e4e9c30e66
|
fix(frontends/lean/builtin_cmds): print patterns
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
41ff4bc193
|
feat(library/blast/forward/pattern): pattern inference and heuristic instantiation index
|
2015-11-25 23:45:08 -08:00 |
|
Leonardo de Moura
|
0ceaf0b4fe
|
feat(frontends/lean/builtin_cmds): display '[forward]' annotation for heuristic instantiation lemmas
|
2015-11-25 17:53:13 -08:00 |
|
Leonardo de Moura
|
67a4cd3972
|
feat(frontends/lean): add print [no_pattern] command
|
2015-11-24 18:48:22 -08:00 |
|
Leonardo de Moura
|
a2f43212d6
|
feat(frontends/lean): add '[no_pattern]' attribute
|
2015-11-24 18:48:22 -08:00 |
|
Daniel Selsam
|
21cb409e6c
|
refactor(library/blast/simplifier): move simplifier module into blast
|
2015-11-19 19:43:04 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|
Leonardo de Moura
|
f363975856
|
feat(frontends/lean): add command #congr_rel for testing new congruence lemma for equivalence relations
|
2015-11-17 18:45:22 -08:00 |
|
Leonardo de Moura
|
8e4fd50913
|
chore(frontends/lean/builtin_cmds): fix style
|
2015-11-16 16:10:01 -08:00 |
|
Leonardo de Moura
|
7abb0d6b96
|
chore(frontends/lean/builtin_cmds,library/blast/simplifier): fix style
|
2015-11-16 11:10:12 -08:00 |
|
Daniel Selsam
|
5e8068b2b2
|
feat(library/blast/simplifier): draft of fusion
|
2015-11-16 09:13:07 -08:00 |
|
Leonardo de Moura
|
ff73fb22fb
|
feat(library/user_recursors): store whether recursor is recursive or not
|
2015-11-15 12:37:35 -08:00 |
|
Daniel Selsam
|
f17320eccf
|
fix(library/abstract_expr_manager): remove weight and lt
|
2015-11-12 21:21:52 -08:00 |
|
Daniel Selsam
|
3703938e55
|
feat(library/abstract_expr_manager): compare exprs ignoring subsingletons
|
2015-11-12 21:21:51 -08:00 |
|
Daniel Selsam
|
031979cb49
|
feat(library/blast/simplifier): take simp_rule_sets as argument
|
2015-11-12 21:20:16 -08:00 |
|
Leonardo de Moura
|
8f378db661
|
feat(library/blast): add normalize procedure to blast API
|
2015-11-12 20:42:58 -08:00 |
|
Leonardo de Moura
|
e1f81cfdcd
|
feat(library/type_context): add normalizer for type_context
|
2015-11-12 20:31:36 -08:00 |
|
Leonardo de Moura
|
9aaa2d0991
|
feat(frontends/lean): add new command for testing new congruence lemmas
Remark: #congr_simp is the old command, and #congr is the new one.
|
2015-11-12 18:55:25 -08:00 |
|
Leonardo de Moura
|
9a557958f4
|
refactor(library/blast): merge state and branch classes
We will keep only one active branch in blast.
All other branches are implicit.
|
2015-11-09 13:24:30 -08:00 |
|
Leonardo de Moura
|
1d1f043192
|
refactor(library/app_builder): throw exception instead of returning none_expr
|
2015-11-08 14:05:03 -08:00 |
|
Leonardo de Moura
|
f74e8288bd
|
refactor(library/congr_lemma_manager): API
|
2015-11-08 14:05:03 -08:00 |
|
Daniel Selsam
|
f3caeb77cd
|
style(library/blast/simplifier): whitespace
|
2015-11-08 14:05:03 -08:00 |
|
Daniel Selsam
|
6c2c82f47c
|
feat(library/blast/simplifier): conditional rewriting
|
2015-11-08 14:05:03 -08:00 |
|
Daniel Selsam
|
8e5e8e6540
|
feat(library/blast/simplifier): basic infrastructure
|
2015-11-08 14:05:02 -08:00 |
|
Leonardo de Moura
|
3dc8f72c32
|
feat(frontends/lean/builtin_cmds): display congr lemma arg mask
|
2015-11-08 14:05:02 -08:00 |
|
Leonardo de Moura
|
8a7321714a
|
feat(library/congr_lemma_manager): add mk_congr_simp that takes the number of expected arguments
Use sorry to be able to test first part
|
2015-11-08 14:05:02 -08:00 |
|
Leonardo de Moura
|
9b34526030
|
feat(frontends/lean): add #congr debugging command
|
2015-11-08 14:05:02 -08:00 |
|
Leonardo de Moura
|
2482c49729
|
test(frontends/lean): add #replace command for debugging purposes
|
2015-11-08 14:05:01 -08:00 |
|
Leonardo de Moura
|
d1fa547335
|
feat(frontends/lean/builtin_cmds): change mask notation at #app_builder command
|
2015-11-08 14:05:01 -08:00 |
|
Leonardo de Moura
|
f21102a725
|
feat(frontends/lean): add test commands for new app_builder features
|
2015-11-08 14:05:01 -08:00 |
|
Leonardo de Moura
|
ee0974650a
|
feat(library/app_builder): new app_builder on top of type_context
The new version is more robust, and invokes type class resolution if needed.
|
2015-11-08 14:05:00 -08:00 |
|
Leonardo de Moura
|
a26ea2a249
|
feat(frontends/lean/builtin_cmds): add command for testing app_builder
|
2015-11-08 14:05:00 -08:00 |
|
Leonardo de Moura
|
ee347772d7
|
feat(library/meng_paulson): ignore class and class-instances when computing set of relevant theorems
|
2015-11-08 14:04:56 -08:00 |
|
Leonardo de Moura
|
023ec1ba76
|
feat(library): add Meng&Paulson heuristic for selecting theorems
|
2015-11-08 14:04:56 -08:00 |
|
Leonardo de Moura
|
d64b410bbd
|
feat(library): add declaration statistics
|
2015-11-08 14:04:56 -08:00 |
|