Leonardo de Moura
|
db5d0d52c5
|
feat(library/tactic): add helper functions
|
2016-06-13 11:58:55 -07:00 |
|
Leonardo de Moura
|
5459e9ad8a
|
chore(frontends/lean): remove dead code
|
2016-06-13 10:42:38 -07:00 |
|
Leonardo de Moura
|
f86f8b040f
|
feat(library/tactic): add 'by' annotation
|
2016-06-13 10:12:00 -07:00 |
|
Leonardo de Moura
|
21bf883fa5
|
feat(library/tactic/tactic_state,library/init/meta): add helper tactics (context, num_goals, repeat, repeat_at_most, repeat_exactly), rename main_type ==> target
|
2016-06-11 21:15:00 -07:00 |
|
Leonardo de Moura
|
c0edb143b4
|
fix(library/tactic/tactic_state): missing return
|
2016-06-11 20:31:04 -07:00 |
|
Leonardo de Moura
|
4c6de9f8e4
|
fix(library/metavar_context): incorrect assertions
|
2016-06-11 20:29:10 -07:00 |
|
Leonardo de Moura
|
bc47eca2ff
|
fix(library/lazy_abstraction): incorrect assertion
|
2016-06-11 20:28:54 -07:00 |
|
Leonardo de Moura
|
125a80ad69
|
feat(library/tactic): add 'clear' tactic
|
2016-06-11 20:23:24 -07:00 |
|
Leonardo de Moura
|
6829c81f18
|
feat(library/tactic): add 'rename' tactic
|
2016-06-11 19:18:25 -07:00 |
|
Leonardo de Moura
|
a732e8ec30
|
feat(library/tactic/tactic_state): add 'unify_core' where user can specify transparency mode
|
2016-06-11 19:14:23 -07:00 |
|
Leonardo de Moura
|
5245a25f89
|
feat(library/tactic/tactic_state): add basic tactics for inferring types, unifying terms, etc
|
2016-06-11 10:51:33 -07:00 |
|
Leonardo de Moura
|
303ef37a23
|
chore(library/tactic): naming conventions and expose APIs
|
2016-06-11 10:23:49 -07:00 |
|
Leonardo de Moura
|
62116f5b4b
|
feat(library/tactic): add 'revert' tactic
|
2016-06-11 10:12:43 -07:00 |
|
Leonardo de Moura
|
aec52b702d
|
chore(library/tactic/tactic_state.h): style
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
fe2b75aac7
|
fix(frontends/lean/pp,library/pp_options): 'pp.all true' should display binder types
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
0a6cc0ab5a
|
feat(library/tactic): assumption tactic
|
2016-06-10 18:29:41 -07:00 |
|
Leonardo de Moura
|
c5d56be4ee
|
fix(library/local_context): typo
|
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
|
cf284ce3eb
|
fix(library/lazy_abstraction): missing case
|
2016-06-10 18:29:40 -07:00 |
|
Leonardo de Moura
|
0ccac266be
|
fix(library/type_context): use get_pp_name
|
2016-06-10 18:29:40 -07:00 |
|
Leonardo de Moura
|
b0b008d0bd
|
feat(library): add lazy_abstraction macro
|
2016-06-10 18:29:40 -07:00 |
|
Leonardo de Moura
|
e9ae5019ca
|
feat(library/tactic): init intro tactic
|
2016-06-10 18:29:19 -07:00 |
|
Leonardo de Moura
|
6e7b4129e7
|
chore(library): add helper functions
|
2016-06-09 16:01:39 -07:00 |
|
Leonardo de Moura
|
4cbcb34817
|
feat(library/init): add combinators SKI
|
2016-06-09 14:39:20 -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
|
91204d4456
|
refactor(library/tactic/tactic_state): move tactic_state_format_expr to tactic_state module
|
2016-06-09 11:02:46 -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
|
831a887bdb
|
feat(library/init/meta/format): add trace_fmt
|
2016-06-09 10:51:49 -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
|
0261a81eb0
|
feat(frontends/lean): add '()' as notation for unit.star
|
2016-06-08 17:26:48 -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
|
165d45ac32
|
fix(library/compiler/erase_irrelevant): monad.return was renamed to monad.ret
|
2016-06-08 16:17:33 -07:00 |
|
Leonardo de Moura
|
cf073f5ed0
|
feat(library/tactic): add tactic_state
|
2016-06-08 15:12:22 -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
|
376bc8a090
|
feat(library/vm): expose 'declaration' C++ object
|
2016-06-07 15:38:48 -07:00 |
|
Leonardo de Moura
|
7ff06e1b2c
|
feat(library/meta): exceptional monad
|
2016-06-07 15:19:43 -07:00 |
|
Leonardo de Moura
|
36c61bc0fb
|
refactor(library/init): cmp_result => ordering
|
2016-06-07 10:14:07 -07:00 |
|
Leonardo de Moura
|
aeee79da2b
|
chore(library): library/tactic => library/old_tactic
|
2016-06-06 16:38:27 -07:00 |
|
Leonardo de Moura
|
2eafe66240
|
fix(library/compiler/lambda_lifting): relax assertion
|
2016-06-06 14:11:05 -07:00 |
|
Leonardo de Moura
|
6157c66ac3
|
feat(library/vm/vm): allow vm_external subclasses to use their own memory allocation policy
|
2016-06-06 12:50:55 -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
|
5cb998ce5f
|
feat(library/type_context): relax assertion
|
2016-06-06 10:54:05 -07:00 |
|
Leonardo de Moura
|
a55a936db2
|
feat(library/vm): expose C++ 'expr' object
|
2016-06-05 21:13:00 -07:00 |
|
Leonardo de Moura
|
1f8c58415e
|
feat(library/vm): expose C++ 'level' object
|
2016-06-05 12:55:57 -07:00 |
|
Leonardo de Moura
|
7da3fe024a
|
feat(library/vm/vm_rb_map): add rb_map.fold
|
2016-06-03 17:32:53 -07:00 |
|
Leonardo de Moura
|
9eb9be2911
|
fix(library/vm/vm): make sure objects are not garbage collected at invoke_cfun when the VM stack is resized
|
2016-06-03 17:31:47 -07:00 |
|
Leonardo de Moura
|
b5ca231cdf
|
fix(library/vm/vm): problems detected when using valgrind
|
2016-06-03 16:55:01 -07:00 |
|