Leonardo de Moura
|
f018fdabb9
|
refactor(library/kernel_bindings): remove unnecessary procedure
|
2015-02-07 18:57:46 -08:00 |
|
Leonardo de Moura
|
1640568f6a
|
refactor(library/reducible): use default_converter in reducible, and converters based on reducible hints
|
2015-02-07 17:31:53 -08:00 |
|
Leonardo de Moura
|
b4f1029318
|
refactor(library/reducible): define opaque_type_checker using default_converter
|
2015-02-07 17:05:29 -08:00 |
|
Leonardo de Moura
|
e04250f0d8
|
refactor(library/tactic/rewrite_tactic): use default_converter
|
2015-02-07 16:44:51 -08:00 |
|
Leonardo de Moura
|
c04c0e8381
|
refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation
|
2015-02-07 15:19:41 -08:00 |
|
Leonardo de Moura
|
7945b8adab
|
refactor(kernel/type_checker): remove useless procedures
|
2015-02-07 14:55:36 -08:00 |
|
Leonardo de Moura
|
c2a296b1de
|
feat(library/tactic/apply_tactic): add flag for disabling class instance resolution in the apply tactic
|
2015-02-06 17:27:24 -08:00 |
|
Leonardo de Moura
|
1557a579ed
|
feat(library/tactic/proof_state): add report_failure flag to proof state
tactic can use the flag to produce nice error messages
|
2015-02-06 16:29:04 -08:00 |
|
Leonardo de Moura
|
2126b8ec9a
|
feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic
closes #360
|
2015-02-06 16:14:03 -08:00 |
|
Leonardo de Moura
|
18808d133e
|
refactor(library/tactic/goal): move goal => local_context conversion to goal class
|
2015-02-06 16:09:59 -08:00 |
|
Leonardo de Moura
|
f10424d729
|
fix(library/tactic/rewrite_tactic): memory leak
|
2015-02-06 15:24:09 -08:00 |
|
Leonardo de Moura
|
aa70334f8d
|
feat(library/tactic/rewrite_tactic): add "fold" step
|
2015-02-06 15:21:49 -08:00 |
|
Leonardo de Moura
|
47bd5e53e2
|
fix(library/tactic/rewrite_tactic): memory leak
|
2015-02-06 14:24:10 -08:00 |
|
Leonardo de Moura
|
7aac9f1fdb
|
feat(library/tactic/rewrite_tactic): use expensive convertability checker at reduce_to steps and trivial goal
|
2015-02-06 13:53:03 -08:00 |
|
Leonardo de Moura
|
5b2a9dacc2
|
fix(library/tactic/rewrite_tactic): matcher should unfold only reducible constants
|
2015-02-06 13:44:04 -08:00 |
|
Leonardo de Moura
|
b4139627e5
|
feat(library/tactic/rewrite_tactic): add option to prevent any kind of constant unfolding when perfoming pattern matching in the rewrite tactic
|
2015-02-06 13:27:33 -08:00 |
|
Leonardo de Moura
|
62daf73dd0
|
chore(library/normalize): fix style
|
2015-02-06 13:27:10 -08:00 |
|
Leonardo de Moura
|
ba9557bb94
|
fix(library/tactic/rewrite_tactic): incorrect assertion
|
2015-02-06 13:02:50 -08:00 |
|
Leonardo de Moura
|
ba641d7c58
|
feat(library/normalize): validate unfold-c hints
|
2015-02-06 12:42:53 -08:00 |
|
Leonardo de Moura
|
7205382f8c
|
feat(library/definitional/projection): add "unfold-c" hint to projections
|
2015-02-06 12:39:57 -08:00 |
|
Leonardo de Moura
|
1bd1f94542
|
feat(library/normalize): add "unfold-c" hint to normalizer
This hint will also be used in the simplifier
|
2015-02-06 12:39:49 -08:00 |
|
Leonardo de Moura
|
39446a7215
|
refactor(library/projection): move is_constructor_app to util
|
2015-02-06 12:12:25 -08:00 |
|
Leonardo de Moura
|
2e626b29fb
|
feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step
|
2015-02-06 11:03:36 -08:00 |
|
Leonardo de Moura
|
264cedb3a6
|
fix(frontends/lean/rewrite_tactic): incorrect assertion
|
2015-02-05 20:02:49 -08:00 |
|
Leonardo de Moura
|
e17ba27596
|
fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter
The solution is not very satisfactory. I should investigate it more.
|
2015-02-05 19:08:47 -08:00 |
|
Leonardo de Moura
|
ffe0d1186e
|
feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic
|
2015-02-05 13:59:55 -08:00 |
|
Leonardo de Moura
|
116c65bff5
|
feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic
|
2015-02-05 13:42:50 -08:00 |
|
Leonardo de Moura
|
7cdc88701d
|
feat(library/tactic/rewrite_tactic): add "reduction" step to rewrite tactic
|
2015-02-05 13:16:05 -08:00 |
|
Leonardo de Moura
|
808521223b
|
feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic
|
2015-02-05 12:58:30 -08:00 |
|
Leonardo de Moura
|
d6958be7e7
|
fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences
|
2015-02-05 10:50:40 -08:00 |
|
Leonardo de Moura
|
941b493835
|
chore(library/tactic/rewrite_tactic): modify param name
|
2015-02-05 10:04:03 -08:00 |
|
Leonardo de Moura
|
0abfa30ead
|
fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements
|
2015-02-05 10:01:18 -08:00 |
|
Leonardo de Moura
|
14c72e82f6
|
feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses
|
2015-02-04 20:04:19 -08:00 |
|
Leonardo de Moura
|
55fb678db2
|
fix(library/tactic/location): clang++ 3.3 compilation problem
|
2015-02-04 18:48:23 -08:00 |
|
Leonardo de Moura
|
42c2f7eb11
|
fix(library/tactic/rewrite_tactic): memory leak
|
2015-02-04 18:40:11 -08:00 |
|
Leonardo de Moura
|
89fde9d829
|
feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic
The idea is to avoid nontermination.
|
2015-02-04 16:13:15 -08:00 |
|
Leonardo de Moura
|
dc297865d4
|
chore(library/tactic/rewrite_tactic): fix compilation warnings
|
2015-02-04 15:34:02 -08:00 |
|
Leonardo de Moura
|
ee079d12f4
|
feat(library/tactic/rewrite_tactic): remove trivial goal in rewrite_tactic
|
2015-02-04 15:29:52 -08:00 |
|
Leonardo de Moura
|
f0fac1ae0e
|
feat(library/constants): add eq.intro
|
2015-02-04 15:27:18 -08:00 |
|
Leonardo de Moura
|
e5381679d6
|
feat(library/tactic/rewrite_tactic): rewrite goal
|
2015-02-04 15:17:58 -08:00 |
|
Leonardo de Moura
|
09818adf90
|
feat(library/tactic/rewrite_tactic): elaborate rewrite rule using unifier
|
2015-02-04 13:51:32 -08:00 |
|
Leonardo de Moura
|
49323ab598
|
feat(library/util): add mk_symm
|
2015-02-04 13:44:55 -08:00 |
|
Leonardo de Moura
|
ccae014ef9
|
feat(library/tactic/rewrite_tactic): ignore inst_implicit arguments when matching applications of declarations which contain them
|
2015-02-04 12:14:47 -08:00 |
|
Leonardo de Moura
|
0e05c239a5
|
feat(library/tactic/rewrite_tactic): add custom matcher pluging for rewriter
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
d6a7ec4621
|
chore(library/tactic/rewrite_tactic): fix style
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
b4dd2cc729
|
refactor(library/tactic/rewrite_tactic): more general rewrite step
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
461fd45efc
|
feat(frontends/lean): allow a different location for each rewrite element
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
c845e44777
|
feat(frontends/lean): parse rewrite tactic
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
180cda304e
|
feat(library/tactic): add rewrite tactic skeleton
The tactic has not been implemented yet, but this commit adds all the
support for storing arguments, serializing and deserializing them.
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
8a78adc9af
|
feat(library/tactic): add auxiliary object "location"
This object will used to specify the scope of application of tactics
|
2015-02-04 11:51:39 -08:00 |
|
Leonardo de Moura
|
420da8fd3f
|
feat(library/projection): store bit saying whether a projection is for a class or not.
|
2015-02-04 08:54:20 -08:00 |
|
Leonardo de Moura
|
c92f3bec65
|
refactor(library/definitional/projection): move projection "database" to library/projection
|
2015-02-04 07:18:43 -08:00 |
|
Leonardo de Moura
|
0e06f4aedc
|
feat(library/match): extend match_plugin interface
|
2015-02-03 18:10:38 -08:00 |
|
Leonardo de Moura
|
44e575c895
|
feat(library/match): improve match_app_core
|
2015-02-03 17:37:22 -08:00 |
|
Leonardo de Moura
|
790fd9c24b
|
chore(library/match): remove unused procedure
|
2015-02-03 15:20:26 -08:00 |
|
Leonardo de Moura
|
f79f43c702
|
refactor(library/match): use "special" meta-variables instead of free variables to represent placholders in the higher-order matcher
|
2015-02-03 15:15:04 -08:00 |
|
Leonardo de Moura
|
45e62031e2
|
fix(library/match): bug in matcher
|
2015-02-03 13:46:19 -08:00 |
|
Leonardo de Moura
|
4c7a17cc4a
|
refactor(library/tactic/class_instance_synth): move has_expr_metavar_relaxed to util
|
2015-02-01 10:59:27 -08:00 |
|
Leonardo de Moura
|
c311e0aba6
|
chore(library/tactic/inversion_tactic): cleanup
|
2015-02-01 10:47:32 -08:00 |
|
Leonardo de Moura
|
143143e94c
|
fix(library/tactic/inversion_tactic): missing normalization step in the inversion_tactic
|
2015-02-01 10:38:30 -08:00 |
|
Leonardo de Moura
|
e9e1f86b7f
|
fix(library/app_builder): many bugs, add use_cache option, add tests
|
2015-01-29 15:30:31 -08:00 |
|
Leonardo de Moura
|
e6f022e3f2
|
fix(library/match): index out of bounds
|
2015-01-29 14:41:38 -08:00 |
|
Leonardo de Moura
|
b5d1f4e54c
|
feat(library/match): add low-level match API
|
2015-01-29 14:09:09 -08:00 |
|
Leonardo de Moura
|
f587cc3e1d
|
feat(library/app_builder): expose app_builder API in Lua
|
2015-01-29 11:38:56 -08:00 |
|
Leonardo de Moura
|
5efd91e435
|
fix(library/app_builder): missing initialization
|
2015-01-29 11:38:28 -08:00 |
|
Leonardo de Moura
|
5bb2a41c64
|
feat(library/reducible): expose Lua API for reducible hints
|
2015-01-29 10:37:15 -08:00 |
|
Leonardo de Moura
|
4cf2dcaa7e
|
feat(library/app_builder): add helper class for creating applications efficiently using type inference
The idea is to use this class in the simplifier.
For example, we will use to create: symmetry, reflexivity, transitivity
and congruence proof steps.
|
2015-01-28 18:40:21 -08:00 |
|
Leonardo de Moura
|
4e08cc0659
|
feat(library/match): add flag for tracking whether matcher assigned anything
|
2015-01-28 18:39:50 -08:00 |
|
Leonardo de Moura
|
dbc8e9e13a
|
refactor(*): add method get_num_univ_params
|
2015-01-28 17:22:18 -08:00 |
|
Leonardo de Moura
|
5aaade47d8
|
feat(library/match): add new API
|
2015-01-28 16:42:42 -08:00 |
|
Leonardo de Moura
|
a1eeb0a6a1
|
fix(library/print): typo in is_used_name
closes #408
|
2015-01-25 08:58:08 -08:00 |
|
Leonardo de Moura
|
27f6bfd3f0
|
refactor(*): add file constants.txt with all constants used by the Lean binary
|
2015-01-23 16:50:32 -08:00 |
|
Leonardo de Moura
|
880faf89e0
|
feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command
closes #354
|
2015-01-21 18:12:29 -08:00 |
|
Leonardo de Moura
|
a53098385c
|
refactor(frontends/lean/type_util): move infer_implicit_params to library
|
2015-01-21 17:22:41 -08:00 |
|
Leonardo de Moura
|
1d6ff5f761
|
feat(library/definitional/projection): throw exception if unsupported case occurs
The user can workaround it by using trust-level 0 (i.e., no option -t num or -T)
|
2015-01-20 17:42:34 -08:00 |
|
Leonardo de Moura
|
01ce57e52e
|
feat(library/definitional/projection): add projection macro
|
2015-01-20 16:21:50 -08:00 |
|
Leonardo de Moura
|
b6750e9d29
|
feat(library/util): add auxiliary functions
|
2015-01-20 15:44:58 -08:00 |
|
Leonardo de Moura
|
8355ed55d7
|
refactor(library/definitional/projection): remove dead code
|
2015-01-20 13:40:09 -08:00 |
|
Leonardo de Moura
|
752b54085b
|
refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used
Now, we unfold untrusted macros outside of the Lean kernel.
|
2015-01-20 12:36:56 -08:00 |
|
Leonardo de Moura
|
2717adde94
|
feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant
|
2015-01-19 16:23:29 -08:00 |
|
Leonardo de Moura
|
d0e9e0e21c
|
feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors
|
2015-01-18 20:58:40 -08:00 |
|
Leonardo de Moura
|
858d21f20b
|
feat(library/definitional/projection): store projection information
|
2015-01-18 16:26:56 -08:00 |
|
Leonardo de Moura
|
6c07ca5d41
|
perf(library/print): improve is_used_name
|
2015-01-15 19:01:13 -08:00 |
|
Leonardo de Moura
|
8ab775bd6f
|
feat(*): distinguish between logical and runtime exceptions.
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
|
2015-01-15 16:54:55 -08:00 |
|
Leonardo de Moura
|
ef529c660f
|
fix(library/definitional/no_confusion): mark no_confusion as reducible
Auxiliary definitions should be marked as reducible
|
2015-01-13 18:44:47 -08:00 |
|
Leonardo de Moura
|
e9338669dc
|
feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages
|
2015-01-13 13:30:12 -08:00 |
|
Leonardo de Moura
|
41935906a8
|
chore(frontends/lean): use update_if_undef
|
2015-01-13 13:02:14 -08:00 |
|
Leonardo de Moura
|
e5a8c67d22
|
fix(library/definitional/equations): assertion violation
|
2015-01-13 11:57:14 -08:00 |
|
Leonardo de Moura
|
1fbfe59a9a
|
feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line
closes #391
|
2015-01-13 11:14:44 -08:00 |
|
Leonardo de Moura
|
a3bc1b0cd5
|
fix(library/definitional/equations): add more equation validation to avoid obscure error message
|
2015-01-09 18:52:21 -08:00 |
|
Leonardo de Moura
|
2e4a2451e6
|
refactor(library/reducible): simplify reducible/irreducible semantics
|
2015-01-08 18:52:18 -08:00 |
|
Leonardo de Moura
|
698754b2bb
|
feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases
|
2015-01-08 12:00:47 -08:00 |
|
Leonardo de Moura
|
f344dd75c4
|
feat(library/pp_options): add get_pp_purify_locals_name
|
2015-01-08 11:55:08 -08:00 |
|
Leonardo de Moura
|
5c118127ae
|
fix(library/definitional/equations): memory access violation
|
2015-01-07 17:06:41 -08:00 |
|
Leonardo de Moura
|
597f7385e8
|
fix(library/unifier): incorrect fix
|
2015-01-07 16:57:02 -08:00 |
|
Leonardo de Moura
|
15b5344626
|
feat(library/definitional/equations): copy tags
|
2015-01-07 14:00:46 -08:00 |
|
Leonardo de Moura
|
2990a6d029
|
fix(library/unifier): missing "set_conflict" in process_delta
|
2015-01-07 12:41:01 -08:00 |
|
Leonardo de Moura
|
760dc2162a
|
chore(library/definitional/equations): cleanup
|
2015-01-06 14:53:21 -08:00 |
|
Leonardo de Moura
|
a3a6697f44
|
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
|
2015-01-06 14:07:17 -08:00 |
|
Leonardo de Moura
|
c33928f202
|
fix(library/pp_options): memory leak
|
2015-01-06 10:22:23 -08:00 |
|