michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8006 commits 3 branches 0 tags 28 MiB
Commit graph

221 commits

Author SHA1 Message Date
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
Leonardo de Moura
5051c0031e feat(frontends/lean): add '#accessible' command for debugging purposes 2015-09-30 18:50:28 -07:00