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
Leonardo de Moura
ea43f3ea80
fix(frontends/lean/builtin_cmds): fixes #630
2015-05-26 22:19:42 -07:00
Floris van Doorn
a127a676eb
fix(tests): fix tests to reflect changes
2015-05-26 21:37:02 -07:00
Leonardo de Moura
0502f46f9b
fix(frontends/lean/scanner): another bug related to issue #626
2015-05-26 13:39:42 -07:00
Leonardo de Moura
25e41b9b09
fix(frontends/lean/scanner): fixes #626
2015-05-26 11:33:38 -07:00
Leonardo de Moura
a4e72e5262
test(tests/lean/run): add missing test
2015-05-25 17:02:23 -07:00
Leonardo de Moura
d0987eb3ac
feat(library/tactic): add 'subtvars' tactic
2015-05-25 16:36:44 -07:00
Leonardo de Moura
ab58e538a4
feat(frontends/lean/elaborator): hide auxiliary 'match' hypothesis during elaboration
2015-05-25 15:24:56 -07:00
Leonardo de Moura
a3f23d5233
feat(library/tactic): add improved 'subst' tactic
2015-05-25 15:03:59 -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
88975927e6
fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol
2015-05-24 18:56:35 -07:00
Leonardo de Moura
004ea80e65
fix(library/tactic/rewrite_tactic): apply beta reduction when selecting patterns
2015-05-24 18:44:30 -07:00
Jeremy Avigad
8bebd104ff
refactor(library/*): remove 'Module:' lines
2015-05-23 20:52:23 +10:00
Jeremy Avigad
db7bdce451
refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function
2015-05-23 16:16:36 +10:00
Leonardo de Moura
b83b0c0017
fix(library/tactic/induction_tactic): fixes #619
2015-05-21 18:22:07 -07:00
Leonardo de Moura
89581cead7
fix(frontends/lean/parser): fixes #616
2015-05-20 23:33:41 -07:00
Leonardo de Moura
d6b72ef4d7
feat(library/tactic/induction_tactic): try available recursors until one works
...
closes #615
2015-05-20 23:23:05 -07:00
Leonardo de Moura
2164ba6f20
fix(library/tactic/induction_tactic): fixes #614
2015-05-20 23:14:11 -07:00
Leonardo de Moura
51d4644832
fix(library/tactic/induction_tactic): fixes #613
2015-05-20 22:26:50 -07:00
Leonardo de Moura
5508e4b132
feat(library/tactic/induction_tactic): type class inference for minor premises
...
closes #611
2015-05-20 20:48:33 -07:00
Leonardo de Moura
029f374a69
fix(library/tactic/induction_tactic): fixes #610
2015-05-20 20:28:02 -07:00
Leonardo de Moura
2d22bb8ea2
feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command
...
In the future, we should probably add an option for unfolding proofs.
2015-05-20 19:14:57 -07:00
Leonardo de Moura
d5da659be7
feat(frontends/lean/elaborator): include overload information in error messages
2015-05-20 17:21:27 -07:00
Leonardo de Moura
76c3757db7
feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type
...
closes #547
2015-05-20 16:12:12 -07:00
Leonardo de Moura
af3f0088f4
feat(frontends/lean): add 'override' (notation) command
2015-05-20 11:42:16 -07:00
Leonardo de Moura
8ce992b077
feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode
2015-05-19 16:26:02 -07:00
Leonardo de Moura
c133d26505
feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics
...
Unresolved placeholders were not being reported
2015-05-19 16:23:50 -07:00
Leonardo de Moura
78ee055de8
feat(library/tactic): add induction tactic with support for user defined recursors
...
closes #483
closes #492
2015-05-19 13:27:17 -07:00
Leonardo de Moura
6da2ba331f
fix(library/user_recursors): memory access violation
2015-05-19 11:07:31 -07:00
Leonardo de Moura
937d6ac7b6
fix(frontends/lean/pp): print notation produces incorrect output
...
fixes #604
2015-05-19 09:57:13 -07:00
Leonardo de Moura
e1c2340db2
fix(frontends/lean): consistent behavior for protected declarations
...
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608
closes #609
2015-05-18 22:35:18 -07:00
Leonardo de Moura
c53b96c8d3
feat(frontends/lean): print all options for overloaded identifier
...
closes #608
2015-05-18 17:14:17 -07:00
Floris van Doorn
1c77122fd0
fix(tests): update tests because [unfold-c] attribute has been added to some definitions
2015-05-18 15:59:55 -07:00
Leonardo de Moura
19361f0196
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
...
see discussion at #604
2015-05-18 15:45:23 -07:00
Leonardo de Moura
c61c049152
feat(library/user_recursors): generalize acceptable use-defined recursors
...
see issue #492
2015-05-18 14:21:10 -07:00
Leonardo de Moura
62082c72a8
fix(library/user_recursors): remove unnecessary restriction on minor premises of user-defined recursors
...
see issue #492
2015-05-18 10:09:11 -07:00
Leonardo de Moura
830d0ce1a7
fix(library/user_recursors): make sure homotopy.rec_on is recognized as a valid user-defined recursor
...
see issue #492
2015-05-18 09:57:50 -07:00
Leonardo de Moura
d4da381e1a
feat(tests/lean/run/tut_104): add extra test
2015-05-14 18:34:48 -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
1dedd2829c
fix(library/match): bug in higher-order matcher
2015-05-14 18:27:10 -07:00
Leonardo de Moura
7f8afcf04b
fix(frontends/lean/builtin_exprs): bug in 'using' expressions
2015-05-14 17:17:48 -07:00
Sebastian Ullrich
77c20e99ff
feat(library/tactic/inversion_tactic): consistent orientation of generated equalities
...
Generated equalities in proof irrelevant environments were inverted
compared with the documentation and the proof relevant case, which
resulted in newly generated local vars replacing equivalent old ones
instead of the other way around.
2015-05-14 23:32:54 +02:00
Leonardo de Moura
ea7694ca32
fix(tests/lean/slow/path_groupoids): to reflect changes in the libraries
2015-05-13 22:32:07 -07:00
Leonardo de Moura
cbcaf5a48e
fix(frontends/lean/scanner): block comments
...
fixes #600
2015-05-13 22:14:28 -07:00
Leonardo de Moura
163577c23a
fix(library/normalize): fixes #599
2015-05-13 18:36:16 -07:00
Leonardo de Moura
e0b39079eb
test(tests/lean/extra): add test for issue #597
2015-05-13 15:34:34 -07:00
Leonardo de Moura
11fbee269b
fix(frontends/lean/parser): must save state of name_generator in parser snapshot
...
To provide typing and auto-completion information, we create a
background process by starting lean with the option --server.
In "server" mode, we create snapshots of the parser state.
The idea is to be able to quickly reprocess a file when the user makes a
modification. This commit fixes a bug in the snapshot operation.
It was not saving in the snapshots the unique name generator used by the parser.
By creating a fresh name generator, we may accidentally
assign the same internal name to two different constants.
This bug triggered the crash described in issue #593 .
This commit fixes the test in the comment
https://github.com/leanprover/lean/issues/593#issuecomment-101768484
This commit also adds a smaller version of the problem to the test suite
2015-05-13 12:28:23 -07:00
Leonardo de Moura
f403ea984b
feat(frontends/lean): add 'print [recursor]' command for debugging purposes
2015-05-12 15:48:24 -07:00
Leonardo de Moura
750f6d5a43
feat(library,frontends/lean): validate user defined recursors and add attribute to mark them
...
see issue #492
The user-defined recursors will also be used to implement the blast tactic
2015-05-12 15:48:01 -07:00
Leonardo de Moura
3d8586088b
fix(frontends/lean/elaborator): problem with 'calc' proofs discussed at issue #592
2015-05-11 13:22:39 -07:00
Leonardo de Moura
d636b34c1c
fix(tests/lean): make sure tests do not fail when compiling Lean with cmake option "-DIGNORE_SORRY=ON"
2015-05-11 11:49:23 -07:00
Leonardo de Moura
c5fb3ec6d0
fix(library/definitional/equations): fixes #541
...
This commit allows recursive applications to have less or more arguments
than the equation left-hand-side.
We add two tests
- 541a.lean recursive call with more arguments
- 542b.lean recursive call with less arguments
2015-05-10 20:37:44 -07:00
Leonardo de Moura
8f711873a0
fix(tests/lean): adjust tests to reflect changes in the pretty printer
2015-05-10 11:10:38 -07:00
Leonardo de Moura
9812cfe906
test(tests/lean/run): add example for constructive choice
2015-05-09 12:02:52 -07:00
Leonardo de Moura
e9c8de7bdf
feat(frontends/lean): remove unnecessary option
2015-05-09 11:49:55 -07:00
Leonardo de Moura
d217655a62
fix(kernel/quotient/quotient): bug in reduction rule for quot.ind
2015-05-09 09:07:03 -07:00
Leonardo de Moura
4e35afedcc
feat(frontends/lean): rename 'wait' to 'reveal'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-05-08 20:54:16 -07:00
Leonardo de Moura
f8e2f68ce0
feat(frontends/lean): add 'wait' command
...
This commit also fixes several problems with -j option (parallel
compilation). The .olean files were not missing data when -j was used
see issue #576
2015-05-08 20:05:21 -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
57ea660963
refactor(*): start process for eliminating of opaque
definitions from the kernel
...
see issue #576
2015-05-08 16:06:04 -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
72663e8a06
feat(library/tactic/rewrite_tactic): take hypotheses into account when checking rewrite step
2015-05-08 11:34:50 -07:00
Leonardo de Moura
746e6dc0ff
fix(tests/lean): adjust tests output to reflect recent changes in the pretty printer
2015-05-08 11:11:00 -07:00
Floris van Doorn
ae43b244ef
fix(tests): fix tests to reflect recent changes
2015-05-07 16:39:04 -07:00
Leonardo de Moura
eb3a236119
fix(library/unifier): typo
...
fixes #588
2015-05-07 16:30:02 -07:00
Leonardo de Moura
f6a1d1c864
fix(frontends/lean/parser): fixes #584
2015-05-07 14:24:30 -07:00
Leonardo de Moura
aff9257c72
feat(frontends/lean): allow → to be used in calc proofs
...
see issue #586
2015-05-07 12:28:47 -07:00
Leonardo de Moura
b03266be70
feat(library/normalize,frontends/lean): rename '[unfold-m]' hint to '[constructor]', and allow it to be attached to constants
...
closes #587
2015-05-07 12:00:34 -07:00
Leonardo de Moura
5113f6b9d8
fix(tests/lean): test output to reflect recent changes
2015-05-07 10:01:28 -07:00
Leonardo de Moura
ac24f19210
fix(library/tactic/rewrite_tactic): use relaxed type checker when processing rewrite "proof step"
...
That is, the restricted type checker should only be used in the
matching/unification step.
fixes #583
2015-05-07 09:57:23 -07:00
Leonardo de Moura
5798ac43de
fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors
...
fixes #582
2015-05-07 09:09:07 -07:00
Leonardo de Moura
171530d5cc
fix(frontends/lean/notation_cmd): fixes #585
2015-05-07 08:36:37 -07:00
Leonardo de Moura
16b7bc3922
fix(kernel/default_converter): broken optimization
...
we must also check the universe levels when applying the optimization for
constraints of the form:
f.{l_1 ... l_k} a_1 ... a_n =?= f.{l_1' ... l_k'} b_1 ... b_n
The optimization tries to avoid unfolding f if we can establish that
a_i is definitionally equal to b_i for each i in [1, n]
closes #581
2015-05-06 18:32:41 -07:00
Leonardo de Moura
02662fe489
test(tests/lean/run/new_obtain4): test new 'obtain' expression using minimal amount of annotations
2015-05-06 12:51:06 -07:00
Leonardo de Moura
613281d622
fix(frontends/lean/builtin_exprs): bug in new 'obtain' expression
2015-05-06 10:01:24 -07:00
Leonardo de Moura
26c662accd
feat(frontends/lean/builtin_exprs): improve new 'obtain' expression
2015-05-06 09:56:57 -07:00
Leonardo de Moura
84deddcca9
feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution
2015-05-05 20:23:49 -07:00
Leonardo de Moura
c7a20644c0
fix(library/tactic/rewrite_tactic): bug in rewrite tactic (HoTT mode)
...
closes #580
2015-05-05 19:25:15 -07:00
Leonardo de Moura
a4efefb6ff
feat(library/tactic/rewrite_tactic): display type error message when
...
rewrite tactic fails
2015-05-05 19:23:41 -07:00
Leonardo de Moura
9bb8c5c98a
test(tests/lean/hott): test 'obtain' in the HoTT library
2015-05-05 18:57:09 -07:00
Leonardo de Moura
7cd444882c
feat(frontends/lean): add 'begin+' and 'by+' that enter tactic mode with the whole context visible
2015-05-05 18:47:25 -07:00
Leonardo de Moura
5d515a06f7
test(tests/lean/run): add test showing that "proof ... qed" can access the whole context
2015-05-05 18:32:47 -07:00
Leonardo de Moura
616f49c2e4
feat(frontends/lean): improved 'obtains' expression
2015-05-05 18:30:16 -07:00
Leonardo de Moura
741fca1e7b
feat(hott/init/path): mark 'idp' and 'idpath' with '[unfold-m]' hint
...
closes #496
2015-05-04 14:29:22 -07:00
Leonardo de Moura
6571c47353
feat(library/normalize): add '[unfold-m]' hint
...
See issue #496
2015-05-04 14:23:04 -07:00
Leonardo de Moura
b347f4868b
test(tests/lean/eq_class_error): save "workaround" for cryptic error message
2015-05-03 21:08:09 -07:00
Leonardo de Moura
87aaf373f4
fix(frontends/lean): fix '#' override notation on the left-hand-side of recursive equations (and match-expressions)
2015-05-03 21:08:09 -07:00
Leonardo de Moura
326048df54
feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic
...
see discussion at:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc
2015-05-02 19:33:59 -07:00
Leonardo de Moura
441f1f9fe2
feat(frontends/lean): import error message for "unknown" tactics when parsing
2015-05-02 18:57:58 -07:00
Leonardo de Moura
118189eaac
fix(frontends/lean/elaborator): bug in translation function
...
This commit fixes the bug reported in the lean discussion list:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc
2015-05-02 18:05:07 -07:00
Leonardo de Moura
e1dc18f6b6
fix(library/tactic/inversion_tactic): check whether eliminator can only eliminate to Prop
...
fixes #571
2015-05-02 17:48:08 -07:00
Leonardo de Moura
e379034b95
feat(library/tactic): improve 'assumption' tactic
...
- It uses the unifier in "conservative" mode
- It only affects the current goal
closes #570
2015-05-02 17:33:54 -07:00
Leonardo de Moura
8c107d6936
fix(frontends/lean/builtin_cmds): bug in export
command
...
Cause: we have two different tokes to represent declarations: [decls] and [declarations]
fixes #568
2015-05-02 16:01:25 -07:00
Leonardo de Moura
b39fe17dee
feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics
...
closes #500
2015-05-02 15:48:25 -07:00
Leonardo de Moura
cd17618f4a
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
...
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
2015-05-02 15:15:35 -07:00
Leonardo de Moura
efc33a2f1d
fix(tests/lean): adjusts tests
2015-05-02 13:01:37 -07:00
Leonardo de Moura
415ca2b93f
feat(library/tactic): add 'congruence' tactic
...
It is the f_equal described at issue #500 .
2015-05-02 12:58:46 -07:00
Leonardo de Moura
230b994e79
fix(tests/lean/slow): adjust tests
2015-05-01 19:47:55 -07:00
Leonardo de Moura
9dc0388022
fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses
2015-05-01 19:45:23 -07:00
Leonardo de Moura
ac8ba6a3cf
feat(library/tactic): add 'subst' tactic
...
see issue #500
2015-05-01 19:31:24 -07:00
Leonardo de Moura
b0759f3986
fix(library/tactic/rewrite_tactic): bug when rewriting multiple hypotheses
2015-05-01 19:03:43 -07:00
Leonardo de Moura
ea87dd48e3
chore(tests/lean/hott/inj_tac): fix typo
2015-05-01 18:18:57 -07:00
Leonardo de Moura
de369a0a0a
feat(library/tactic/injection_tactic): improve 'injection' tactic
...
see issue #500
2015-05-01 15:49:56 -07:00
Leonardo de Moura
9ba8b284a1
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
2015-05-01 15:08:00 -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
7e9f574ef3
fix(library/tactic/apply_tactic): use internally 'apply' instead of 'fapply' as the default "apply" tactic
...
This changes improves the 'constructor' tactic
2015-04-30 21:58:35 -07:00
Leonardo de Moura
4f7f66de3f
test(tests/lean/run): add new test
2015-04-30 21:38:33 -07:00
Leonardo de Moura
2d9c950144
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
...
see issue #500
2015-04-30 21:15:07 -07:00
Leonardo de Moura
15e52b06df
fix(library/tactic/constructor_tactic): bug in constructor tactic
...
see example (constr_tac2.lean) in comment at issue #500
2015-04-30 20:18:24 -07:00
Leonardo de Moura
d18f9c7607
fix(library/tactic/constructor_tactic): use 1 (instead of 0) to reference the first constructor
...
see comment at issue #500
2015-04-30 20:08:00 -07:00
Leonardo de Moura
0b995c4fe3
fix(library/tactic/rewrite_tactic): relax reducibility constraints in some parts of the rewrite tactic
...
fixes #567
2015-04-30 18:22:58 -07:00
Leonardo de Moura
d152f38518
feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics
...
see issue #500
2015-04-30 17:52:29 -07:00
Leonardo de Moura
125ab8c228
fix(tests/lean/interactive/findp): adjust test output
2015-04-30 15:45:15 -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
3233008039
feat(library/tactic): allow user to name generalized term in the 'generalize' tactic
...
closes #421
2015-04-30 11:57:40 -07:00
Leonardo de Moura
3912bc24c8
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
2015-04-30 11:00:39 -07:00
Leonardo de Moura
d6d30f12c6
feat(frontends/lean): add "polymorphic" print command
...
closes #524
2015-04-29 16:17:33 -07:00
Leonardo de Moura
1a28a3c36f
feat(frontends/lean): add 'print inductive' command
2015-04-29 15:22:10 -07:00
Leonardo de Moura
dce7177382
feat(library/tactic/change_tactic): improve 'change' tactic
...
- Better error messages
- Try to solve unification constraints produced during is_def_eq test
addresses comment on issue #531
2015-04-29 13:31:09 -07:00
Leonardo de Moura
d055947243
feat(library/tactic/rewrite_tactic): ignore implicit argument when matching at rewrite tactic
2015-04-29 12:51:33 -07:00
Leonardo de Moura
b790ca9806
fix(library/tactic/rewrite_tactic): type check rewriting steps
...
closes #550
2015-04-29 12:16:37 -07:00
Leonardo de Moura
d1cb0018c0
fix(tests): adjust tests to reflect changes in the HoTT library
2015-04-29 10:15:13 -07:00
Leonardo de Moura
051615712c
fix(kernel/quotient/quotient): bug in reduction rule
2015-04-29 10:01:17 -07:00
Leonardo de Moura
d2c7b5c319
feat(library/tactic): add 'let' tactic
...
closes #555
2015-04-28 17:24:43 -07:00
Leonardo de Moura
1be72f1faa
feat(frontends/lean): parse argument of unary tactis with rbp=0, tokens may have a different precedence in expression and tactic modes
2015-04-28 13:43:05 -07:00
Leonardo de Moura
a23118d357
feat(frontends/lean): add tactic_notation command
...
This addresses the first part of issue #461
We still need support for tactic definitions
2015-04-27 17:46:13 -07:00
Leonardo de Moura
ca8943f45b
feat(library,hott): remove rapply tactic
2015-04-27 15:06:16 -07:00
Leonardo de Moura
9d01868361
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
...
closes #502
2015-04-24 17:23:12 -07:00
Leonardo de Moura
28404fe16d
fix(library/tactic/rewrite_tactic): second problem reported at issue #548
...
closes #548
2015-04-24 16:49:32 -07:00
Leonardo de Moura
6134c8822a
fix(frontends/lean/util): assertion violation
...
fixes #559
2015-04-24 15:09:23 -07:00
Leonardo de Moura
f723550d33
feat(frontends/lean/elaborator): decorates error message with free variables introduced by the left-hand-side of the equation
...
closes #528
2015-04-24 14:58:15 -07:00
Leonardo de Moura
8241863abe
feat(kernel/hits): add two builtin HITs: type_quotient and trunc
2015-04-23 15:32:31 -07:00
Leonardo de Moura
2613e7c444
fix(frontends/lean): bug when handling identifiers in tactics
...
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
2015-04-22 16:03:22 -07:00
Leonardo de Moura
e1a609cad9
fix(tests/lean/interactive/findp): test output to reflect changes in the stdlib
2015-04-22 13:08:56 -07:00
Leonardo de Moura
349cdb3fe7
test(tests/lean): add test showing that the binder type update should not change the parameter order
2015-04-22 13:04:05 -07:00
Leonardo de Moura
a526cd92ac
fix(frontends/lean): bug in pretty printer
...
this is related to issue #530
2015-04-22 12:44:08 -07:00
Leonardo de Moura
dc93603b4a
feat(frontends/lean): parameter and variable binder type update
...
see issue #532
2015-04-22 12:28:11 -07:00
Leonardo de Moura
91f21c007a
feat(frontends/lean): remove 'context' command
2015-04-22 11:32:02 -07:00
Leonardo de Moura
53653c3526
fix(frontends/lean): pretty printing in sections with parameters
...
fix #530
2015-04-21 22:44:09 -07:00
Leonardo de Moura
8e9997e253
chore(tests/lean/interactive/sec_info_bug): remove 'context' command from test
2015-04-21 19:52:01 -07:00
Leonardo de Moura
fe9f4dd95f
fix(frontends/lean): another bug in sections with parameters
2015-04-21 19:50:21 -07:00
Leonardo de Moura
3df99e514b
fix(frontends/lean): problems with sections
2015-04-21 19:46:57 -07:00
Leonardo de Moura
9fb7aa9f1c
chore(tests): remove most occurrences of 'context' command from the test suite
2015-04-21 19:33:21 -07:00
Leonardo de Moura
ce153d01f9
test(tests/lean/sec_notation2): notation nested in namespace/section/section
2015-04-21 19:07:52 -07:00
Leonardo de Moura
52e9ad1a98
feat(frontends/lean): allow persistent notation declaration in sections (when they do not contain parameters)
...
see issue #554
2015-04-21 19:04:06 -07:00
Leonardo de Moura
bf8a7eb9b4
fix(library/scoped_ext): bug in local metadata in sections
...
The problem is described in issue #554
2015-04-21 18:56:28 -07:00
Leonardo de Moura
697a536d9e
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic
...
fixes #545
2015-04-20 19:24:52 -07:00
Leonardo de Moura
107763a506
fix(frontends/lean): better error message for 'proof ... qed' blocks containing unsolved placeholders
2015-04-20 15:50:37 -07:00
Leonardo de Moura
6f6d106a10
feat(library/tactic): add "check_expr" tactic
...
closes #486
2015-04-19 19:00:05 -07:00
Leonardo de Moura
60e320fd79
feat(frontends/lean): protected constants and axioms
...
fixes #527
2015-04-19 17:45:58 -07:00
Leonardo de Moura
b7ca2a0ec9
fix(library/tactic/exact_tactic): exact and or_else
...
fixes #543
2015-04-19 17:23:09 -07:00
Leonardo de Moura
306087b5d3
refactor(library/data): rename 'countable' to 'encodable', define countable in the usual way, and prove all 'encodable' type is 'countable'
2015-04-19 14:20:47 -07:00
Leonardo de Moura
cc63a40a01
feat(library): enforce name conventions on old nat declarations
2015-04-18 10:50:30 -07:00
Leonardo de Moura
3e5796acb2
fix(tests/lean/abbrev1): to reflect recent changes
2015-04-18 10:40:46 -07:00
Leonardo de Moura
f16eaf8f0f
test(tests/lean/run/pickle1): add unpickle/pickle test
2015-04-14 21:32:07 -07:00
Leonardo de Moura
795acc70a6
refactor(library/data/finset): move finset to its own directory
2015-04-09 19:30:09 -07:00
Leonardo de Moura
4416d9b2c5
test(tests/lean/run): add basic tests for finset module
2015-04-09 15:56:41 -07:00
Leonardo de Moura
24f1454c0a
fix(tests/lean/interactive/findp): adjust test output to reflect recent changes in the pretty printer
2015-04-08 09:49:22 -07:00
Leonardo de Moura
5d95cb0979
feat(library/tactic): add 'refine' tactic
...
closes #482
2015-04-06 18:36:56 -07:00
Leonardo de Moura
412f03b08b
feat(library/tactic/exact_tactic): generate error if 'exact' tactic produces a term containing metavariables
2015-04-06 13:38:53 -07:00
Leonardo de Moura
754276a660
feat(frontends/lean): round parenthesis for [tactic1 | tactic2]
...
This commit also replaces the notation for divides
`(` a `|` b `)`
with
a `∣` b
The character `∣` is entered by typing \|
closes #516
2015-04-06 09:24:09 -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
bebe8a4f17
fix(tests/lean/bad_coercions): expected output
2015-04-05 03:00:29 -07:00
Leonardo de Moura
d731a4ab13
feat(library/normalize): add '[unfold-f]' hint
...
closes #497
2015-04-05 03:00:13 -07:00
Leonardo de Moura
d591c63840
feat(frontends/lean/decl_cmds): allow local coercions in contexts
...
closes #525
2015-04-04 15:25:07 -07:00
Leonardo de Moura
8c59f17605
feat(frontends/lean): 'using' expression without 'show' or 'have'
...
closes #536
2015-04-04 15:25:07 -07:00
Leonardo de Moura
4ec0e1b07c
feat(frontends/lean): improve calc mode
...
Now, it automatically supports transitivity of the form
(R a b) -> (b = c) -> R a c
(a = b) -> (R b c) -> R a c
closes #507
2015-04-04 08:58:35 -07:00
Leonardo de Moura
1150b19598
perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables
2015-04-02 23:37:33 -07:00
Leonardo de Moura
f8023403af
test(tests/lean/run): add another simple test
2015-04-01 15:49:01 -07:00
Leonardo de Moura
bf142f3f18
fix(tests/lean): adjust tests to reflect changes in the standard library
2015-04-01 15:09:00 -07:00
Leonardo de Moura
0d66d19ba3
feat(tests/lean/run/finset): show that if A has decidable equality, then (finset A) also has it.
2015-04-01 13:19:16 -07:00
Leonardo de Moura
b960e123b1
feat(kernel): add experimental support for quotient types
2015-03-31 22:04:16 -07:00
Leonardo de Moura
82833bcbe8
fix(tests/lean/struct_class): add setoid to expected output
2015-03-31 22:03:57 -07:00
Leonardo de Moura
8c76419c60
fix(frontends/lean/decl_cmds): error localization problem for recursive equations
2015-03-30 13:30:29 -07:00
Leonardo de Moura
ec1a60b02c
feat(library/init/logic): add helper function for proving decidable equality
2015-03-30 02:14:26 -07:00
Soonho Kong
8243ed6339
fix(test*.sh): allow spaces in filename
...
fix #515
2015-03-28 23:29:52 -04:00
Leonardo de Moura
75621df52b
feat(frontends/lean): uniform notation for lists in tactics
...
closes #504
2015-03-27 17:54:48 -07:00
Leonardo de Moura
242f8ba048
feat(frontends/lean/elaborator): include number of unsolved goals
...
See #509
2015-03-27 14:54:41 -07:00
Leonardo de Moura
0c3fd7427e
feat(frontends/lean): add syntax-sugar for fold
...
closes #503
2015-03-25 18:25:48 -07:00
Leonardo de Moura
f2b1752807
fix(frontends/lean/parser): add workaround for #461
2015-03-25 18:09:43 -07:00
Leonardo de Moura
b9e3c474c9
feat(library/tactic): add all_goals tactic
...
closes #501
2015-03-25 17:42:34 -07:00
Leonardo de Moura
49bc56ec07
feat(frontends/lean/pp): improve pretty printer for prefix and postfix notation
...
closes #491
2015-03-25 16:45:58 -07:00
Leonardo de Moura
a1f933886f
fix(frontends/lean/structure_cmd): explicit universe levels for structures
...
closes #490
2015-03-25 16:10:30 -07:00
Leonardo de Moura
33d2e8d9d3
test(tests/lean/run): workaround for issue #505
2015-03-25 15:53:50 -07:00
Leonardo de Moura
5f1d827b26
fix(frontends/lean/decl_cmds): assertion violation
...
closes #506
2015-03-25 13:46:23 -07:00
Leonardo de Moura
ac30052a29
fix(library/tactic/rewrite_tactic): apply substitution before trying to rewrite
...
closes #487
2015-03-23 18:32:52 -07:00
Leonardo de Moura
5bf46d1226
fix(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT mode
...
closes #481
2015-03-23 18:06:11 -07:00
Leonardo de Moura
76157ba392
fix(frontends/lean/pp): abbreviations with too much arguments
...
closes #480
2015-03-23 12:16:25 -07:00
Leonardo de Moura
0814e76298
fix(library/tactic/clear_tactic): unexpected failure
...
This commit also improves the error message produced by the 'clear' tactic.
fixes #488
2015-03-23 12:08:15 -07:00
Leonardo de Moura
35f2a61b4d
fix(tests/lean): add missing file
2015-03-23 11:35:39 -07:00
Leonardo de Moura
b5acbb2228
fix(frontends/lean/pp): missing parenthesis around abbreviations
...
fixes #476
2015-03-16 17:12:03 -07:00
Leonardo de Moura
fc3a7bac59
feat(frontends/lean): improve error handling inside match-with expressions
2015-03-13 23:25:46 -07:00
Leonardo de Moura
bed0d6df6b
fix(frontends/lean/elaborator): inaccessible over coercion
2015-03-13 23:04:45 -07:00
Leonardo de Moura
cfeb426cd7
fix(frontends/lean): pretty print numeral notation from algebra
2015-03-13 18:58:34 -07:00
Leonardo de Moura
362a0ec04c
test(tests/lean): tests for error handling improvements
2015-03-13 15:32:25 -07:00
Leonardo de Moura
b88b98ac22
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
...
The idea is to avoid a "tsunami" of error messages when a heavily used
theorem breaks in the beginning of the file
2015-03-13 14:47:21 -07:00
Leonardo de Moura
f5811d6092
feat(frontends/lean): hide subterms that do not contain metavariables
...
when generating "unresolved metavariables" error message
closes #473
2015-03-13 12:42:57 -07:00
Leonardo de Moura
cda19f5aa6
feat(library/tactic/rewrite_tactic): improve rewrite tactic error messages
...
closes #471
2015-03-12 20:49:53 -07:00
Leonardo de Moura
7accd0f1e6
feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders
...
see discussion at #470
2015-03-12 18:07:55 -07:00
Leonardo de Moura
3e4d849a4a
refactor(kernel/metavar.h): simplify API
2015-03-12 12:50:53 -07:00
Leonardo de Moura
6a78ae7b46
fix(library/tactic/class_instance_synth): enforce consistent behavior in type class resolution
...
Auxiliary procedure mk_class_instance was not discarding partial solutions.
This procedure is used by the apply and inversion (aka cases) tactics
2015-03-12 10:27:05 -07:00
Leonardo de Moura
47a350d888
fix(library/tactic/inversion_tactic): missing condition for applying optimization
2015-03-12 09:11:36 -07:00
Leonardo de Moura
7de3d5771d
feat(library/tactic/rewrite_tactic): add eta-reduction support at esimp
...
closes #469
2015-03-12 00:32:31 -07:00
Leonardo de Moura
b5fb7c734e
feat(library/tactic/inversion_tactic): remove hypothesis being destructed
...
addresses second issue in #468
2015-03-11 20:42:50 -07:00
Leonardo de Moura
4c6b0dc0e5
fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account
...
fixes #466
2015-03-11 08:49:59 -07:00
Leonardo de Moura
4904f7657f
test(tests/lean/run): add definition package tests
2015-03-09 08:42:21 -07:00
Leonardo de Moura
f6cd604a44
chore(library/data/bool): enforce naming conventions
2015-03-06 19:20:48 -08:00
Leonardo de Moura
f966634910
feat(frontends/lean): nested dependent pattern matching
2015-03-06 19:18:08 -08:00
Leonardo de Moura
14ca2d407d
test(tests/lean/run): add match-with nested in tactic test
2015-03-06 17:47:01 -08:00
Leonardo de Moura
1490bdad49
feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration
2015-03-06 17:34:45 -08:00
Leonardo de Moura
bd8c4315f1
feat(frontends/lean): allow 'match-with' to be used in tactics without prefixing it with 'exact'
2015-03-06 15:49:31 -08:00
Leonardo de Moura
4edd7b9099
fix(library/definitional/equations): allow a function to be the result of a match-with term or recursive definition
2015-03-06 15:08:52 -08:00
Leonardo de Moura
f24d9e84fe
feat(frontends/lean): add option 'max_memory'
...
Default value is 512Mb
2015-03-06 13:56:20 -08:00
Leonardo de Moura
3b721fe675
feat(frontends/lean): add missing 'help' command
2015-03-06 13:56:20 -08:00
Leonardo de Moura
daf36803c4
fix(frontends/lean/builtin_exprs): bug in 'using' construct
2015-03-06 13:56:20 -08:00
Leonardo de Moura
368f9d347e
refactor(frontends/lean): approach used to parse tactics
...
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
2015-03-05 18:11:21 -08:00
Leonardo de Moura
28487ede3b
feat(frontends/lean/decl_cmds): allow 'empty' set of pattern matching equations
2015-03-05 14:37:29 -08:00
Leonardo de Moura
b73a931c70
fix(frontends/lean/elaborator): missing case 'no-equation' annotation
2015-03-05 14:37:29 -08:00
Leonardo de Moura
039afb4578
feat(frontends/lean): treat "proof t qed" as alias for "by exact t"
2015-03-05 11:12:39 -08:00
Leonardo de Moura
abd238aef0
feat(*): add [quasireducible] attribute
2015-03-04 22:12:49 -08:00
Leonardo de Moura
c6d15dc198
fix(tests/lean/interactive): adjust tests to reflect changes in the standard library
2015-03-04 18:30:31 -08:00
Leonardo de Moura
fde83cd376
fix(tests/lean/hott): adjust tests to reflect changes in the libraries
2015-03-04 09:28:16 -08:00
Leonardo de Moura
18e6e55fc9
chore(tests/lean/interactive/num2): adjust test to reflect changes in the standard library
2015-03-03 16:17:59 -08:00
Leonardo de Moura
fa79b214b8
fix(frontends/lean): allow 'attribute <id> [priority ...]'
2015-03-03 16:17:32 -08:00
Leonardo de Moura
3b73e100dc
test(tests/lean/run): add [priority] test using num.sub
2015-03-03 15:59:17 -08:00
Leonardo de Moura
efd096e85c
feat(library/init/num): define sub and le for binary numerals
2015-03-03 15:55:16 -08:00
Leonardo de Moura
11aad4449b
feat(frontends/lean): add '[semireducible]' attribute
...
This commit also renames the elements of reducible_status.
The idea is to use in the C++ implementation the same names used in the
Lean front-end.
2015-03-03 10:48:36 -08:00
Leonardo de Moura
b254c78c44
refactor(library/algebra): move bundled structures to separate module
...
Motivation: performance.
After this commit, the bundled instances do not participate in the
class/instance resolution if we do not import algebra.bundled.
2015-03-02 18:45:08 -08:00
Leonardo de Moura
8240d7adcd
perf(frontends/lean/util): improve univ_metavars_to_params_fn
...
We moved to replace_visitor because it uses a more precise cache.
2015-03-02 18:25:00 -08:00
Leonardo de Moura
c81762970e
fix(frontends/lean/elaborator): revert commit ededf4fc6c
...
The instantiate_all are needed. See issue #457
2015-03-02 13:00:54 -08:00
Leonardo de Moura
ededf4fc6c
feat(frontends/lean): remove unnecessary instantiate_all's that were messing with error localization
2015-03-01 14:51:44 -08:00
Leonardo de Moura
c772d7bf84
fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks
...
Closes #454
2015-02-28 09:03:56 -08:00
Leonardo de Moura
dc62bc498f
fix(tests/lean/hott/443_b): adjust test to reflect changes in the HoTT library
2015-02-28 08:46:00 -08:00
Leonardo de Moura
cf56935b01
feat(frontends/lean): improve support for user defined tactics
2015-02-27 16:58:25 -08:00
Leonardo de Moura
5b736a2268
feat(frontends/lean): add support for empty match-with expressions
2015-02-26 16:36:15 -08:00
Leonardo de Moura
0b48f406f9
fix(tests/lean/hott): adjust tests to reflect changes in the HoTT library
2015-02-26 10:51:19 -08:00
Leonardo de Moura
68110faa4d
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
2015-02-25 17:00:10 -08:00
Leonardo de Moura
5ca52d81ec
feat(frontends/lean): ML-like notation for match and recursive equations
2015-02-25 16:20:44 -08:00
Leonardo de Moura
3c24461e51
refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'
2015-02-25 15:18:21 -08:00
Leonardo de Moura
c04c610b7b
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
2015-02-25 14:30:42 -08:00
Leonardo de Moura
383c0d6d4c
fix(tests/lean/interactive/findp): adjust test to reflect recent changes in the standard library
2015-02-25 14:08:37 -08:00
Jeremy Avigad
e555531eb6
feat(library/data/int/div): start on div for integers
2015-02-25 14:05:07 -08:00
Leonardo de Moura
96b54a8007
feat(frontends/lean/builtin_exprs): add 'have' notation in 'begin-end' blocks
...
It is notation for the assert tactic.
2015-02-25 14:04:17 -08:00
Leonardo de Moura
909ebfc5f1
feat(frontends/lean/elaborator): try coercions after each overload
...
We try only the easy cases since the more general case is too expensive.
closes #444
2015-02-24 17:41:20 -08:00
Leonardo de Moura
34c36648bb
fix(frontends/lean/decl_cmds): constants command
...
closes #445
2015-02-24 16:27:13 -08:00
Leonardo de Moura
42289d4334
feat(library/tactic/class_instance_synth): create class instance synthesis subproblems only for arguments marked with the []
binder annotation
2015-02-24 16:12:39 -08:00
Leonardo de Moura
3ede8e9150
refactor(library): use []
binder annotation when declaring instances
2015-02-24 16:12:39 -08:00
Leonardo de Moura
1cd44e894b
feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible
...
closes #442
2015-02-24 16:12:35 -08:00
Leonardo de Moura
275068641e
fix(tests/lean/print_ax2): adjust test output
2015-02-24 13:34:52 -08:00
Leonardo de Moura
4364b7f926
feat(frontends/lean): pp.beta is true by default
...
Remark: there is one exception (command: print definition). For this
command pp.beta is still false.
2015-02-24 12:27:53 -08:00
Leonardo de Moura
1ff6446a63
feat(frontends/lean): nested begin-end blocks
2015-02-24 11:59:27 -08:00
Leonardo de Moura
dc2ac92846
fix(library/definitional/equations): use whnf on recursive definition arguments
...
The idea is to expose "hidden" datatypes.
2015-02-23 22:27:30 -08:00
Leonardo de Moura
787fed95aa
fix(library/tactic/inversion_tactic): bug in simpler case (hypotheses were being lost)
2015-02-23 16:10:49 -08:00
Leonardo de Moura
7adecaf494
fix(frontends/lean/structure_cmd): include context/section parameteres/variables that are used in explicit structure parameters
2015-02-23 15:28:43 -08:00
Leonardo de Moura
923fed8612
fix(frontends/lean/structure_cmd): bug in alias generation in the structure command
...
This commit (and 75acb3bc66
) closes #443
2015-02-23 15:17:05 -08:00
Leonardo de Moura
75acb3bc66
fix(frontends/lean/structure_cmd): internal name of parameter/variable was being erased
2015-02-23 15:01:27 -08:00
Leonardo de Moura
7d35d18cad
fix(library/tactic/rewrite_tactic): bug when matching terms that expanded into projections
2015-02-22 18:23:10 -08:00
Leonardo de Moura
753b9dcd75
fix(tests/lean/hott): adjust tests to reflect changes in standard library
2015-02-22 09:39:27 -08:00
Leonardo de Moura
33e562a7ce
fix(frontends/lean/structure_cmd): effect of "include" command in the structure command
...
closes #438
2015-02-19 22:44:51 -08:00
Leonardo de Moura
421a30d75c
feat(library): export [reducible] annotations from function namespace to top-level
...
see issue #433
2015-02-16 18:52:41 -08:00