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
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
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
Leonardo de Moura
7fc216183e
feat(library/tactic): produce better error message when a tactic fails
...
closes #348
2015-02-16 18:42:15 -08:00
Leonardo de Moura
461c02d790
fix(tests/lean/hott/433): remove bogus comment, and use rewrite tactic
...
Fix an issue raised by Floris.
See discussion at
https://github.com/leanprover/lean/issues/433
2015-02-16 15:45:31 -08:00
Leonardo de Moura
4248ad644d
fix(frontends/lean): priority expressions parser
2015-02-14 12:26:06 -08:00
Leonardo de Moura
5cbdd77ad0
feat(library/tactic/rewrite_tactic): improve matcher in rewrite_tactic
...
closes #433
2015-02-13 12:40:55 -08:00
Leonardo de Moura
8ffadce4ab
feat(frontends/lean): add "premise" and "premises" command
...
It is just an alternative notation for "variable" and "variables"
closes #429
2015-02-11 18:46:03 -08:00
Leonardo de Moura
04e92e1e96
feat(frontends/lean/parser): reject explicit universe levels in variables and parameters
...
This modification was motivated by issue #427
2015-02-11 16:25:06 -08:00
Leonardo de Moura
a35cce38b3
feat(frontends/lean): new semantics for "protected" declarations
...
closes #426
2015-02-11 14:09:25 -08:00
Leonardo de Moura
eceed03044
feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command
2015-02-11 11:02:59 -08:00
Leonardo de Moura
1832fb6f54
feat(*): uniform metaclass names, metaclass validation at 'open' command
2015-02-11 10:35:04 -08:00
Leonardo de Moura
9d1cd073c5
feat(frontends/lean): add 'print metaclasses' command
2015-02-11 10:13:20 -08:00
Leonardo de Moura
60fca7575c
fix(frontends/lean/pp): bugs when pretty printing abbreviations
2015-02-10 19:06:09 -08:00
Leonardo de Moura
f9832fb89f
test(tests/lean/abbrev1): add test for abbreviation command
2015-02-10 18:28:48 -08:00
Leonardo de Moura
014271da8b
feat(frontends/lean): better error messages for ill-terminated declarations
2015-02-10 14:38:00 -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