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
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
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
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
Leonardo de Moura
aeee79da2b
chore(library): library/tactic => library/old_tactic
2016-06-06 16:38:27 -07:00
Leonardo de Moura
2a38ddb124
refactor(library): merge util and occurs
2016-03-22 09:51:06 -07:00
Leonardo de Moura
c98f1bfd24
refactor(library): remove type_util module and implement get_num_args using abstract_type_context
2016-03-21 16:30:08 -07:00
Leonardo de Moura
8dde1489f9
refactor(library/util): isolate util procedures that depend on old_type_checker
2016-03-21 13:36:08 -07:00
Leonardo de Moura
128d6cdec2
refactor(library/tactic): remove tactics whnf and beta
2016-03-21 11:48:36 -07:00
Leonardo de Moura
29ad781ec2
refactor(kernel): remove converter class
...
This abstraction is not useful after refactoring.
2016-03-19 15:58:15 -07:00
Leonardo de Moura
487a1e7f89
refactor(kernel): remove extension_context
...
We replaced it with abstract_type_context
2016-03-19 15:15:39 -07:00
Leonardo de Moura
63d8a0ed45
refactor(kernel): move justification/constraint/metavar to library
...
These files will be eventually deleted
2016-03-19 14:39:15 -07:00
Leonardo de Moura
e7f1f409c4
refactor(kernel): simplify kernel type_checker
...
TODO: cleanup, move justification/metavar/constraints to library
2016-03-18 16:28:42 -07:00
Leonardo de Moura
d8079aa16a
refactor(library): create copy of the kernel type_checker in library
...
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
2016-03-18 14:34:10 -07:00
Leonardo de Moura
56d7fc4c23
refactor(*): cleanup replace_visitor subclasses, and make sure let-expressions are handled
2016-02-29 16:55:19 -08:00
Leonardo de Moura
f54963bc3e
refactor(library/tactic/expr_to_tactic): remove 'by_plus' support
2016-02-29 13:50:05 -08:00
Leonardo de Moura
eee74ef1b4
refactor(frontends/lean/pp): use abstract_type_context instead of type_checker
2016-02-26 15:35:29 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
5a4dd3f237
feat(library/reducible): remove [quasireducible] annotation
2016-02-25 17:42:44 -08:00
Leonardo de Moura
146edde5b3
feat(library/class): mark instances as quasireducible by default
...
quasireducible are also known as lazyreducible.
There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
2016-02-25 12:11:29 -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
Floris van Doorn
4e2cc66061
style(*): rename is_hprop/is_hset to is_prop/is_set
2016-02-22 11:15:38 -08:00
Leonardo de Moura
632d4fae36
chore(library): rename local_context to old_local_context
2016-02-11 18:15:16 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Leonardo de Moura
d3242a2068
refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas
2016-01-09 12:32:18 -08:00
Rob Lewis
a57b7fadfb
style(replace_tactic): remove extra whitespace
2016-01-04 15:10:51 -05:00
Rob Lewis
031831f101
feat(library/tactic): add replace tactic
2016-01-04 14:43:31 -05:00
Leonardo de Moura
61ecf018e9
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050
chore(library,hott): enforce naming conventions
2015-12-17 11:36:58 -08:00
Sebastian Ullrich
2185ee7e95
feat(library/tactic): make let tactic transparent, introduce new opaque note tactic
...
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
2015-12-14 10:14:02 -08:00
Leonardo de Moura
193a9d8cde
refactor(library/norm_num): avoid manual constant name initialization
...
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt
Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.
We also have a python script for initializing the C++ name objects.
To use the script:
- go to src/library
- execute
python ../../script/gen_constants_cpp.py constants.txt
It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.
I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.
I found an assertion violation at line 606. Could you take a look?
Best,
Leo
2015-12-13 21:38:59 -08:00
Leonardo de Moura
727a4f5a3a
feat(library/tactic/intros_tactic): use '_' to say that some names are irrelevant in the intro tactic
...
See #695
2015-12-13 16:47:31 -08:00
Leonardo de Moura
d4e49a8434
feat(library/tactic/intros_tactic): intro without argument should introduce a single variable
...
see #695
2015-12-13 16:28:39 -08:00
Leonardo de Moura
894875dc5c
feat(library/tactic/congruence_tactic): closes #855
2015-12-13 15:03:25 -08:00
Leonardo de Moura
7b29ee1666
fix(library/tactic/induction_tactic): fixes #892
2015-12-10 10:52:57 -08:00
Leonardo de Moura
8b3cbb8fdd
fix(library/tactic/induction_tactic): apply substitution to hypothesis type (it may contain metavars)
...
closes #876
2015-12-10 10:11:55 -08:00
Leonardo de Moura
c9ff175cf4
fix(library/tactic/induction_tactic): fixes #893
2015-12-10 10:11:55 -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
