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

48 commits

Author SHA1 Message Date
Leonardo de Moura
4474f0ce44 feat(library/tactic/tactic_state): add pp_goal 2016-07-05 18:35:11 -07:00
Leonardo de Moura
58569b82d3 refactor(frontends/lean,library,library/tactic): move type_context_cache_helper to type_context module 2016-06-30 12:03:40 +01:00
Leonardo de Moura
1c2804256e fix(library/tactic/tactic_state): do not assume combinator.K is in the environment 2016-06-28 16:48:53 +01:00
Leonardo de Moura
48d6319c1c feat(library/init/meta/tactic): add 'when_tracing' tactical 2016-06-28 11:29:39 +01:00
Leonardo de Moura
d524ab013f refactor(library/init/meta): make sure 'transparency' is the first argument 2016-06-28 10:25:38 +01:00
Leonardo de Moura
59f2b9e8c2 refactor(library/type_context): "metavar_context & m_mctx" ==> "metavar_context m_mctx" 2016-06-25 13:08:03 -07:00
Leonardo de Moura
72606479ec feat(library/tactic/tactic_state): add get_tactic_vm_state 2016-06-24 15:56:19 -07:00
Daniel Selsam
e1bc0a68e6 refactor(simplifier): port skeleton to new tactic framework 
Conflicts:
	library/init/meta/tactic.lean
	src/library/tactic/tactic_state.cpp
 2016-06-24 15:20:40 -07:00
Leonardo de Moura
2be8fa646c refactor(library/tactic/defeq_simplifier): move VM binding for defeq_simp 2016-06-24 13:24:11 -07:00
Leonardo de Moura
2b43f591c9 fix(library/type_context): remove m_cache_owner field 
This idiom creates problem if we use (even accidentally) the copy constructor.
 2016-06-23 14:03:46 -07:00
Leonardo de Moura
120c48b1b2 feat(library/tactic): expose congr_lemmas 
This commit also adds several helper code, and fixes bugs in congr_lemma.cpp
 2016-06-22 19:17:08 -07:00
Daniel Selsam
9327d85f6c chore(library/defeq_simplifier): move to new module inside library/tactic 2016-06-22 17:18:57 -07:00
Leonardo de Moura
d03dc18096 chore(library/tactic/tactic_state): add helper methods 2016-06-20 10:47:48 -07:00
Leonardo de Moura
05eafa08eb chore(library/tactic/tactic_state): style 2016-06-18 14:55:47 -07:00
Leonardo de Moura
b546167a64 feat(library/tactic/tactic_state): add tactic mk_fresh_name 2016-06-18 13:02:45 -07:00
Leonardo de Moura
5021b02043 feat(library/init/meta/tactic,library/tactic/tactic_state): add tactics for setting options 2016-06-18 12:05:58 -07:00
Leonardo de Moura
5846dc1812 feat(library/tactic/tactic_state): add get_assignment and get_univ_assignment 2016-06-18 11:34:00 -07:00
Leonardo de Moura
6a0f11f705 feat(library/tactic/tactic_state,library/init/meta/tactic): add mk_meta_univ, mk_meta_var, mk_const 
This commit also changes the semantics of the unify tactic.
It fails if the arguments are not unifiable.
 2016-06-18 11:12:51 -07:00
Leonardo de Moura
735aa4ebfa feat(library/tactic/tactic_state): add 'is_class' and 'apply_instance' tactics 2016-06-18 09:51:02 -07:00
Leonardo de Moura
ded1fe74c5 refactor(library/init/meta/tactic): implement num_goals in Lean 2016-06-17 16:18:15 -07:00
Leonardo de Moura
b21a3376e0 feat(library/init/meta/tactic): add 'focus' and 'all_goals' tacticals 2016-06-17 16:11:40 -07:00
Leonardo de Moura
6371a8db38 fix(library/tactic/tactic_state): consume solved goals 2016-06-17 15:19:50 -07:00
Leonardo de Moura
0b2ed21561 feat(library/init/meta/tactic): add rotate_left and rotate_right tactics 2016-06-17 15:11:08 -07:00
Leonardo de Moura
d0afe0aa99 feat(library/tactic): add 'change' tactic 2016-06-17 13:21:52 -07:00
Leonardo de Moura
2d6742b091 feat(library/tactic): add tactic.defeq_simp 2016-06-17 11:20:15 -07:00
Leonardo de Moura
27085c3d16 feat(library/tactic/tactic_state): add tactic.mk_instance 2016-06-17 08:39:18 -07:00
Leonardo de Moura
7f03684d89 fix(library/tactic/tactic_state): forgot to register tactic.whnf 2016-06-16 18:23:57 -07:00
Leonardo de Moura
586baa4118 feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend 
TODO: invoke elaborator at tactic.to_expr
 2016-06-15 16:06:39 -07:00
Leonardo de Moura
5b8ac6ba30 feat(library/tactic): add 'exact' tactic 2016-06-14 21:30:58 -07:00
Leonardo de Moura
62905152f9 feat(kernel/environment): add is_eqp for environment 2016-06-14 12:28:59 -07:00
Leonardo de Moura
26c10c368a refactor(library): instantiate ==> instantiate_mvars 
Motivation: avoid confusion with 'instantiate' procedure for variables
 2016-06-14 10:29:47 -07:00
Leonardo de Moura
9bcb4e05db feat(library/tactic): store tactic_state at failure 2016-06-13 15:25:55 -07:00
Leonardo de Moura
3962d9b021 fix(library/tactic/tactic_state): VM closure arguments should be in reverse order 2016-06-13 13:23:46 -07:00
Leonardo de Moura
906bb45a44 feat(library/tactic/tactic_state): add format_result tactic 2016-06-13 12:46:41 -07:00
Leonardo de Moura
db5d0d52c5 feat(library/tactic): add helper functions 2016-06-13 11:58:55 -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
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
13bbac8771 feat(library/tactic): intro_tactic and variants 2016-06-10 18:29:41 -07:00
Leonardo de Moura
6e7b4129e7 chore(library): add helper functions 2016-06-09 16:01:39 -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
181e48e3f3 feat(library/tactic/tactic_state): add tactic_state.to_format 2016-06-09 10:47:17 -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
cf073f5ed0 feat(library/tactic): add tactic_state 2016-06-08 15:12:22 -07:00