max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
8893 commits 1 branch 0 tags 5.3 GiB
Commit graph

982 commits

Author SHA1 Message Date
Leonardo de Moura
0a6cc0ab5a feat(library/tactic): assumption tactic 2016-06-10 18:29:41 -07:00
Leonardo de Moura
13bbac8771 feat(library/tactic): intro_tactic and variants 2016-06-10 18:29:41 -07:00
Leonardo de Moura
2df6fb35e6 feat(library/vm): avoid list<A> eager conversion to vm_obj (for A in {name, level, expr}) 2016-06-09 14:16:32 -07:00
Leonardo de Moura
d64a064d32 chore(library/tactic/tactic_state): improve pp_goal 2016-06-09 10:56:58 -07:00
Leonardo de Moura
181e48e3f3 feat(library/tactic/tactic_state): add tactic_state.to_format 2016-06-09 10:47:17 -07:00
Leonardo de Moura
9a63898c51 chore(tests/lean/run): unit.star ==> () 2016-06-09 09:26:36 -07:00
Leonardo de Moura
222f7429e2 feat(frontends/lean/pp): pp unit.star 2016-06-08 17:30:11 -07:00
Leonardo de Moura
790980013a feat(library/init/meta): add 'trace_expr' 2016-06-08 17:27:37 -07:00
Leonardo de Moura
dde4a46fe3 feat(library/vm): add 'trace' 2016-06-08 16:32:20 -07:00
Leonardo de Moura
586e9447d1 feat(frontends/lean/builtin_cmds): add command #tactic for testing new tactic framework 2016-06-08 16:19:41 -07:00
Leonardo de Moura
94ef8e3078 chore(library/init/meta/base_tactic): change or_else notation 2016-06-08 15:12:48 -07:00
Leonardo de Moura
a90926a2d0 feat(library/vm/vm_environment): add rest of environment API 2016-06-07 17:51:04 -07:00
Leonardo de Moura
8f10e18f53 feat(library/vm/vm_environment): expose 'environment.add_inductive' 2016-06-07 17:24:43 -07:00
Leonardo de Moura
b28e724709 feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
Leonardo de Moura
414bdc1abb refactor(library): move 'meta' to 'init' folder 
Motivation: tactic framework should be always available.
 2016-06-06 19:08:07 -07:00
Leonardo de Moura
9c4017e59e feat(library/meta/base_tactic): add base_tactic 2016-06-06 15:26:14 -07:00
Leonardo de Moura
fb6c9f2879 feat(library/vm/vm_expr): add more functions to 'expr' API 2016-06-06 11:26:19 -07:00
Leonardo de Moura
a55a936db2 feat(library/vm): expose C++ 'expr' object 2016-06-05 21:13:00 -07:00
Leonardo de Moura
792040b1a5 feat(library/init/bool): mark bor, band and cond as inline 
The idea is to get short-circuit evaluation for Boolean operators.
 2016-06-05 13:03:33 -07:00
Leonardo de Moura
1f8c58415e feat(library/vm): expose C++ 'level' object 2016-06-05 12:55:57 -07:00
Leonardo de Moura
dac2c39646 feat(library/meta/rb_map): add has_to_string and has_to_format type class instances for rb_map 2016-06-03 17:34:49 -07:00
Leonardo de Moura
1834cab3f2 feat(library/meta): add has_cmp type class 2016-06-03 14:06:46 -07:00
Leonardo de Moura
9a14f7543c feat(library/vm): expose rb_map object 2016-06-03 13:45:06 -07:00
Sebastian Ullrich
9561b45af1 fix(frontends/lean): uniform handling of declaration compound names 
* allow compound names in `namespace` and `structure`
* adjust error messages

Conflicts:
	src/frontends/lean/builtin_tactics.cpp
 2016-06-02 18:13:50 -07:00
Leonardo de Moura
3b57246a62 feat(library/meta/format): add 'pp' helper function 2016-06-02 17:57:29 -07:00
Leonardo de Moura
06cb26176c feat(library/vm): expose C++ options object 2016-06-02 11:46:17 -07:00
Leonardo de Moura
5382a5a556 feat(frontends/lean): allow unbounded recursion in meta_definitions 2016-06-01 09:55:07 -07:00
Leonardo de Moura
e7b47a504e feat(frontends/lean): add meta_definition and meta_constant commands 2016-06-01 09:12:41 -07:00
Leonardo de Moura
d763ea1abf chore(tests/lean/run/IO3): remove unnecessary 'open' 2016-05-25 16:05:39 -07:00
Leonardo de Moura
4b002e5bf0 test(tests/lean/run): add IO test 2016-05-25 16:04:54 -07:00
Leonardo de Moura
0239860ad6 test(tests/lean/run): add another IO test 2016-05-25 15:47:02 -07:00
Leonardo de Moura
2a16b58324 test(tests/lean/run): add another IO test 2016-05-25 14:23:57 -07:00
Leonardo de Moura
e82cb6393f test(tests/lean/run): add IO test 2016-05-25 13:46:05 -07:00
Leonardo de Moura
bf2d2b9feb fix(library/vm,library/compiler,frontends/lean): IO monad support 2016-05-25 13:30:43 -07:00
Leonardo de Moura
4c8360efd8 test(tests/lean/run/vm_eval1): test for efficient interpreter 2016-05-24 12:26:25 -07:00
Leonardo de Moura
18b2b51c8b test(tests/lean/run): make sure well_founded.fix works before optimizing its compilation 2016-05-23 16:50:44 -07:00
Leonardo de Moura
f573ebd0a4 refactor(library): make sure prod.pr1 is a projection 2016-03-25 16:28:29 -07:00
Leonardo de Moura
384e8bf7bf refactor(library): remove unifier_plugin 2016-03-21 17:57:53 -07:00
Leonardo de Moura
9d0dfb8404 refactor(frontends/lean): remove calc_proof_elaborator 2016-03-03 17:22:45 -08:00
Leonardo de Moura
227b548341 refactor(frontends/lean/calc): no overloading in calc steps 2016-03-03 15:00:51 -08:00
Leonardo de Moura
2c70ca83a8 refactor(frontends/lean/calc): remove '{}' notation for eq.subst in calc mode 2016-03-03 14:18:20 -08:00
Leonardo de Moura
d7de521126 refactor(library/class): remove attribute [multiple_instances] and old type class resolution procedure 2016-03-03 13:58:22 -08:00
Leonardo de Moura
4a43e33d45 chore(*): disable big chunk of the standard library and tests 2016-03-03 13:43:08 -08:00
Leonardo de Moura
d84a20d68b remove(frontends/lean/server): FINDG command 2016-03-03 10:12:24 -08:00
Jeremy Avigad
4050892889 refactor(library/*): rename 'compose' to 'comp' 2016-03-02 22:48:05 -05:00
Leonardo de Moura
fbe5188480 refactor(frontends/lean): remove 'by+' and 'begin+' tokens 2016-02-29 13:45:43 -08:00
Leonardo de Moura
b41c65f549 feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking 2016-02-29 12:31:23 -08:00
Leonardo de Moura
101cf1ec4c feat(frontends/lean): remove difference between 'have' and 'assert' 2016-02-29 11:28:20 -08:00
Leonardo de Moura
7d61f640f6 refactor(*): add abstract_type_context class 2016-02-26 14:17:34 -08:00
Leonardo de Moura
1924b2884c refactor(library/tactic): remove 'append' and 'interleave' tacticals 
Preparation for major refactoring in the tactic framework.
 2016-02-24 16:02:16 -08:00