Leonardo de Moura
0dc674e350
fix(tests/lean/630): adjust test to reflect changes in the standard library
2015-06-16 11:33:26 -07:00
Jeremy Avigad
a4a8253f50
refactor(library,hott,tests): rename succ_inj to succ.inj, add abbreviation eq_of_succ_eq_succ
2015-06-15 22:52:38 +10:00
Leonardo de Moura
d8620ef4c9
fix(kernel,library,frontends/lean): improve error messages
...
see #669
2015-06-14 19:44:00 -07:00
Leonardo de Moura
8a85e4ee87
feat(frontends/lean/builtin_cmds): improve print <id>
when <id>
is a not yet revealed theorem
...
We add a remark saying the command `reveal <id>` should be used to
access `<id>` definition.
2015-06-13 12:12:22 -07:00
Leonardo de Moura
591fb91f34
fix(frontends/lean/builtin_cmds): fixes #671
2015-06-13 11:35:03 -07:00
Leonardo de Moura
9fbf267a3f
feat(library/tactic/rewrite_tactic): when 'rewrite' step fails apply esimp and try again
...
closes #670
2015-06-12 19:48:58 -07:00
Leonardo de Moura
3d9b557cfd
feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions
...
closes #484
2015-06-12 17:49:26 -07:00
Leonardo de Moura
7bad9fe554
feat(library/error_handling/error_handling): set 'pp.beta' to false when displaying errors
...
see issue #669
2015-06-12 14:46:51 -07:00
Leonardo de Moura
69be4c720c
fix(library/tactic/subst_tactic): bug in 'subst' tactic
2015-06-12 12:11:44 -07:00
Leonardo de Moura
25cbc5c154
fix(kernel/expr): remove 'cast_binder_info'
...
We should put it back when we decide to implement it.
We also fix the bogus comment at src/frontends/lean/parser.cpp.
see issue #667
2015-06-11 18:11:22 -07:00
Leonardo de Moura
8aa634378e
fix(tests/lean): adjust tests to reflect changes in the standard library
2015-06-10 17:00:47 -07:00
Leonardo de Moura
0b335230d7
test(tests/lean): add test for eta at postprocessing
2015-06-10 16:33:27 -07:00
Leonardo de Moura
8b7dc4e03a
feat(frontends/lean): apply eta-reduction in postprocessing step
...
Perhaps, we should add an option to disable this new feature.
Remark: this commit makes commit 46d418a
redundant.
I'm keeping 46d418a
because we may retract this commit in the future.
2015-06-10 16:29:30 -07:00
Leonardo de Moura
4b91cfccff
feat(frontends/lean/builtin_exprs): make notation ( e : T )
builtin
...
In the previous approach, the following (definitionally equal) term was being generated
(fun (A : Type) (a : A), a) T e
2015-06-10 14:52:59 -07:00
Leonardo de Moura
cff7b7474a
test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded
...
see issue #347
2015-06-09 16:17:29 -07:00
Leonardo de Moura
1bffb89126
fix(library/algebra/function): lean was failing to infer that injective is a decidable predicate for finite types with decidable equality
...
This is an issue reported by Haitao.
2015-06-09 15:30:58 -07:00
Leonardo de Moura
2663c9ab9f
test(tests/lean/run): add test/example
...
add test/example that defines count_vars using tactics and recursors.
see #662 for original definition, and e3a0e62859
for the fix that
allows us to use recursive equations.
The recursive equations are compiled into recursors.
2015-06-09 14:50:15 -07:00
Leonardo de Moura
e3a0e62859
fix(library/unifier): try to generate approximate solution for flex-flex constraints before discarding them
...
fixes #662
2015-06-09 14:36:31 -07:00
Leonardo de Moura
627e05c9e6
fix(library/tactic/rewrite_tactic): improve krewrite
2015-06-08 16:46:28 -07:00
Leonardo de Moura
d6a483fe84
feat(library): add idx_metavar module
2015-06-08 16:02:37 -07:00
Leonardo de Moura
496189feed
feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic
...
See item 4 at
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/oJXwW5wT2Ds/d1Dgr8B-pE0J
See also
https://github.com/leanprover/lean/pull/659
2015-06-08 10:41:30 -07:00
Leonardo de Moura
0e099b5fd8
feat(library/tactic/rewrite_tactic): apply beta&eta reduction before rewriting steps, add option 'rewrite.beta_eta' (default true) to control new feature.
2015-06-06 20:43:52 -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
7db84c7036
refactor(library/data): replace 'fin' with Haitao's 'less_than'
...
The commit also fixes vector to use the new definition.
2015-06-05 10:33:19 -07:00
Leonardo de Moura
c76d92284f
feat(library/pp_options): add 'pp.all' option
2015-06-05 08:41:46 -07:00
Floris van Doorn
7f5caab694
feat(nat): redefine le and lt in the standard library
2015-06-04 20:14:13 -04:00
Floris van Doorn
ff01774fd7
renaming(hit): rename type_quotient to quotient, and quotient to set_quotient
...
This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert
Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to
make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid
name clash the standard library quotient, although I don't know whether that name clash would
matter).
2015-06-04 20:14:13 -04:00
Jeremy Avigad
df69bb4cfc
feat(library/*): add theorems from Haitao on sets and functions, clean up
2015-06-04 11:55:25 -07:00
Leonardo de Moura
134740182d
fix(frontends/lean): fixes #652
2015-06-03 21:53:51 -07:00
Leonardo de Moura
68688ecdf6
fix(library/tactic/subst_tactic): in the standard mode, use dependent elimination in the subst tactic (when needed)
...
Before this commit, the subst tactic was producing an type incorrect
result when dependent elimination was needed (see new test for an example).
2015-06-03 17:36:04 -07:00
Leonardo de Moura
b2f8d2000c
fix(library/simplifier/rewrite_rule_set): avoid compiler specific behavior
2015-06-01 22:23:34 -07:00
Leonardo de Moura
d6997300f1
fix(library/private): use environment fingerprint to compute private decls "unique" identifier
...
fixes #648
2015-06-01 22:21:31 -07:00
Leonardo de Moura
4ace996057
fix(library/simplifier): bug in is_permutation_ceqv
2015-06-01 18:07:31 -07:00
Leonardo de Moura
0fbc944cdd
feat(frontends/lean): add '[rewrite]' attribute
2015-06-01 17:58:24 -07:00
Leonardo de Moura
b6fde68012
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples"
2015-06-01 15:35:28 -07:00
Leonardo de Moura
55608c9b9f
fix(frontends/lean/pp): bug in pp arrow
2015-05-31 17:21:37 -07:00
Leonardo de Moura
ca110012d8
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
...
closes #645
2015-05-30 21:57:28 -07:00
Leonardo de Moura
e5a82ef516
feat(frontends/lean): add option for disabling "coercion lifting"
2015-05-30 17:07:42 -07:00
Leonardo de Moura
6f6848968d
feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case
...
closes #252
2015-05-30 16:44:26 -07:00
Leonardo de Moura
ea9c810fca
feat(frontends/lean/coercion_elaborator): implement "coercion lifting"
...
closes #644
2015-05-30 14:45:14 -07:00
Leonardo de Moura
6d2f37857d
feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands
2015-05-29 16:47:29 -07:00
Leonardo de Moura
0ceedbe69e
fix(library/normalize): fixes #640
2015-05-29 15:58:59 -07:00
Leonardo de Moura
60ff057159
test(tests/lean): add missing test for issue #634
2015-05-29 15:13:43 -07:00
Leonardo de Moura
f48cdccd20
fix(frontends/lean/pp): abbreviation with parameters
...
closes #639
2015-05-29 15:13:31 -07:00
Leonardo de Moura
3b7b268e40
fix(frontends/lean/pp): fixes #634
...
trying again...
2015-05-29 14:07:38 -07:00
Leonardo de Moura
7f12401ea7
fix(frontends/lean/elaborator): save type information for 'obtain' declarations
2015-05-29 10:16:12 -07:00
Leonardo de Moura
7342f342a9
fix(frontends/lean/pp): fixes #634
2015-05-28 19:43:49 -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
85409a59d3
feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants
...
closes #511
2015-05-27 16:32:43 -07:00
Leonardo de Moura
dc6411b903
feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior
...
see issue #632
2015-05-27 14:41:12 -07:00