Leonardo de Moura
60c4384d09
fix(library/compiler/elim_recursors): buggy way to detect recursive arguments
2016-07-06 23:27:04 -07:00
Leonardo de Moura
8333500457
refactor(library): move try_eta to util
2016-06-17 10:29:02 -07:00
Leonardo de Moura
ef8b182fb6
feat(library/util): add get_constructor_idx
2016-05-11 13:16:40 -07:00
Leonardo de Moura
5f9120be63
feat(library/util): add get_contructor_relevant_fields
2016-05-11 13:11:37 -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
9564758965
refactor(library/definitional/no_confusion): use new type_checker to derive no_confusion
2016-03-21 15:40:58 -07:00
Leonardo de Moura
7365c575cd
refactor(library/util): use type_checker at to_telescope
...
The to_telescope abstraction is not very useful for
abstract_type_context.
Reason: Fun/Pi (kernel) procedures are not compatible with abstract_type_context.
2016-03-21 15:34:02 -07:00
Leonardo de Moura
9cf995fae8
refactor(library/util): move more procedures from old_util to util
2016-03-21 14:25:40 -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
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
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
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
c19be9d9e7
feat(library/util): add is_app_of helper function
2016-01-13 13:33:30 -08:00
Leonardo de Moura
403966792d
feat(library/app_builder): add helper heq methods
2016-01-09 12:46:14 -08:00
Leonardo de Moura
fdcdfbf385
feat(library/blast/simplifier/simplifier_actions): only add symplified hypothesis if it is not "true"
2015-12-31 14:25:38 -08:00
Leonardo de Moura
cf61adc5d5
feat(frontends/lean): identifiers starting with '_' are now reserved
2015-12-10 22:32:03 -08:00
Daniel Selsam
6e478696d2
feat(library/blast/unit): preprocessor placeholder
2015-12-04 08:30:04 -08:00
Daniel Selsam
2bf9989bd9
refactor(library/blast/unit): simplify module
2015-12-04 08:30:03 -08:00
Daniel Selsam
eac1ebbf72
feat(library/blast/unit): propagate clauses
2015-11-24 21:16:01 -08:00
Leonardo de Moura
01bde866d6
feat(library/util): add auxiliary recognizers
2015-11-08 14:05:01 -08:00
Leonardo de Moura
34d5882b9a
refactor(library/util): rename old is_eq_rec
2015-11-08 14:05:01 -08:00
Leonardo de Moura
0f631889b7
feat(library/app_builder): add helper methods for creating binary relations, and refl/symm/trans proofs
2015-11-08 14:05:00 -08:00
Leonardo de Moura
b02b3d362f
feat(library/simplifier): add simplifier procedure skeleton
2015-07-21 15:08:56 -07:00
Leonardo de Moura
0b7859f387
feat(library,frontends/lean): add support for projections in the elaborator
...
The idea is to simulate the computation rules such as
pr1 (mk a b) ==> a
in the elaborator
2015-06-26 17:18:29 -07:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
Leonardo de Moura
1cbace9df6
feat(library/tactic/congruence_tactic): add congruence lemma generator
...
The generated congruence theorems ignore arguments that are subsingleton types.
2015-06-05 22:00:10 -07:00
Leonardo de Moura
8a89588079
refactor(library,library/tactic): move auxiliary procedures from tactic to library
2015-06-01 16:19:55 -07:00
Leonardo de Moura
d95c064a29
feat(library/simplifier/ceqv): add to_ceqv procedure
2015-05-27 16:35:56 -07:00
Leonardo de Moura
7d73f4f091
refactor(library,frontends/lean): simplify the creation of custom normalizers
2015-05-27 15:33:20 -07:00
Leonardo de Moura
47e5633498
feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic
2015-05-27 12:07:39 -07:00
Leonardo de Moura
f13ca3cd9a
feat(library/tactic/contradiction_tactic): handle (h1 : p) and (h2 : not p) hypotheses in the contradiction tactic
2015-05-25 10:29:51 -07:00
Leonardo de Moura
84faef5d5d
feat(library/tactic/rewrite_tactic): rewrite tactic with 'iff' lemmas
2015-05-14 18:27:13 -07:00
Leonardo de Moura
163577c23a
fix(library/normalize): fixes #599
2015-05-13 18:36:16 -07:00
Leonardo de Moura
cf7e60e5a6
refactor(kernel): remove "opaque" field from kernel declarations
...
see issue #576
2015-05-08 16:06:16 -07:00
Leonardo de Moura
061e26157e
fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking
2015-05-08 12:41:23 -07:00
Leonardo de Moura
210cae7d6c
fix(library/tactic): we must unfold untrusted macros when type checking intermediate results
...
Example: before this commit, the file librata/data/list/perm.lean would
not type check if the option -t 0 (trust level zero) was provided.
Reason: the intermediate term contained a macro, and macros are not
allowed at trust level zero.
2015-05-06 14:23:58 -07:00
Leonardo de Moura
63eb155c7e
feat(library/tactic): add 'injection' tactic
...
see issue #500
2015-05-01 12:45:21 -07:00
Leonardo de Moura
1c6067bac2
feat(library/tactic): add 'exfalso' tactic
...
see issue #500
2015-04-30 15:43:07 -07:00
Leonardo de Moura
9c8a63caec
feat(library/tactic): add 'contradiction' tactic
...
see issue #500
Remark: this tactic also applies no_confusion to take care of a contradiction
2015-04-30 13:47:40 -07:00
Leonardo de Moura
969d17fd12
fix(frontends/lean/elaborator): class inference in tactic mode with trunc
...
closes #477
2015-04-05 17:47:14 -07:00
Leonardo de Moura
058377c8c6
feat(library/tactic/rewrite_tactic): treat iff.refl as trivial step in the rewrite tactic
2015-02-08 17:27:59 -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
49323ab598
feat(library/util): add mk_symm
2015-02-04 13:44:55 -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
a53098385c
refactor(frontends/lean/type_util): move infer_implicit_params to library
2015-01-21 17:22:41 -08:00
Leonardo de Moura
b6750e9d29
feat(library/util): add auxiliary functions
2015-01-20 15:44:58 -08:00
Leonardo de Moura
98a856373d
feat(library/util): add dec_level auxiliary procedure
2015-01-04 13:25:58 -08:00
Leonardo de Moura
1d79cb9c07
fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library
2014-12-22 09:40:15 -08:00
Leonardo de Moura
2070ac849c
feat(library/util): add get_intro_rule_names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
