Leonardo de Moura
f7bc884ae8
chore(kernel/type_checker): fix compilation warning msgs
2017-12-17 08:44:51 -08:00
Gabriel Ebner
9ef95c9dff
chore(gitignore): ignore autogenerated version.lean file
2017-12-17 15:49:51 +01:00
Gabriel Ebner
860cc95730
fix(library/compiler/rec_fn_macro): do not type-check in non-meta declarations
2017-12-17 15:47:52 +01:00
Leonardo de Moura
e89eece98c
feat(library/init): add lean.version : nat × nat × nat
...
closes #1873
2017-12-15 17:48:26 -08:00
Leonardo de Moura
0252393eb5
doc(library/type_context): relax preconditions for using is_def_eq in new implementation
2017-12-15 17:37:33 -08:00
Leonardo de Moura
91ff183b3e
chore(library): remove out notation for out_param
2017-12-15 15:47:58 -08:00
Leonardo de Moura
f0352d31a1
feat(library/type_context, library): inout ==> out modifier in type class declarations
...
@kha: I decided to implement this change before I start the
type_context modifications. The change did not affect the corelib and
test suite much. The only annoying problem is that `out` cannot be
used to name locals anymore.
2017-12-15 14:46:47 -08:00
Leonardo de Moura
9503ceb832
doc(library/type_context): improve docstring for new design
...
cc @kha
2017-12-15 13:20:26 -08:00
Leonardo de Moura
7106bcf7a5
chore(frontends/lean/inductive_cmds): remove app_builder dependency
2017-12-15 11:35:34 -08:00
Leonardo de Moura
7c1447d615
fix(library/app_builder,library/util): get_level's with slightly different behavior
2017-12-15 11:33:29 -08:00
Leonardo de Moura
aed2c442a3
chore(library/app_builder): add assertion stating that app_builder::mk_app arguments do not contain tmp metavars
2017-12-15 11:22:15 -08:00
Leonardo de Moura
8850099e3d
chore(library/tactic/smt): remove app_builder dependency
2017-12-15 11:18:41 -08:00
Leonardo de Moura
0492e49a3f
fix(library/type_context): fixes #1888
2017-12-15 08:49:45 -08:00
Scott Morrison
a395c26165
chore(.travis.yml): work around change in Travis OS X image
2017-12-15 10:41:09 +01:00
Leonardo de Moura
73c4ea7e35
chore(library/type_context): typos and missing remarks
2017-12-14 18:26:41 -08:00
Leonardo de Moura
f0f2fc42b6
doc(library/type_context): design notes for new type_context
2017-12-14 17:57:28 -08:00
Leonardo de Moura
746134d11c
feat(library/init/meta/interactive): add goal tagging support for by_cases
...
This commit also incorporates changes suggested at commit 84a1911949dec94.
2017-12-13 15:17:13 -08:00
Leonardo de Moura
6eae78da01
chore(library/data/rbtree/insert): provide meaningful names to ins.induction minor premises
...
We use them with `case` tactic.
2017-12-13 14:44:48 -08:00
Leonardo de Moura
6c44dd1b7f
feat(frontends/lean): add hide command
...
cc: @kha
2017-12-13 11:53:21 -08:00
Leonardo de Moura
056a7db7b3
test(tests/lean/run): heap interface experiments
...
They expose limitations in the elaborator.
2017-12-12 18:19:30 -08:00
Mario Carneiro
17f77367cd
chore(library/init/data/fin/ops): revert 107ad36259.
2017-12-12 10:53:12 -08:00
Sean Leather
107ad36259
feat(library/init/data/fin/ops): fin.succ.inj
2017-12-12 04:23:01 -05:00
Leonardo de Moura
cb74ef1670
chore(library/init/meta/interactive): fix docstring
2017-12-11 16:27:04 -08:00
Leonardo de Moura
533ddc0279
fix(library/init/meta/interactive): remove buggy generalizing param from with_cases
2017-12-11 16:27:04 -08:00
Leonardo de Moura
b778d77c0c
chore(doc/changes): with_cases and cases changes, - ==> *
2017-12-11 16:27:04 -08:00
Leonardo de Moura
5217ae735d
feat(library/init/meta/interactive): do not make tag longer when constructor/apply create a single subgoal
2017-12-11 16:27:03 -08:00
Leonardo de Moura
f0231f17bc
feat(library/init/meta): propagate tags in constructor-like tactics
2017-12-11 16:27:03 -08:00
Leonardo de Moura
f18aa1d413
chore(tests/lean): fix tests
2017-12-11 16:27:03 -08:00
Leonardo de Moura
5fa857dc69
fix(library/tactic/tactic_state): do not diplay case for empty tag
2017-12-11 16:27:03 -08:00
Leonardo de Moura
ebeb5f713a
feat(library/init/meta/interactive): do not make tag longer when induction/cases create a single subgoal
2017-12-11 16:27:03 -08:00
Leonardo de Moura
53961b12cb
chore(library/data/rbtree/insert): use new case tactic to cleanup proofs
2017-12-11 16:27:03 -08:00
Leonardo de Moura
8bda71af6f
feat(library/init/meta/interactive): new case tactic with support for with_cases and tagging
2017-12-11 16:27:03 -08:00
Leonardo de Moura
bf8fa50481
feat(library/init/data/list/basic): add is_prefix_of and is_suffix_of
2017-12-11 16:27:03 -08:00
Leonardo de Moura
ddfcc2cb0b
feat(library/init/data/list/basic): define decidable_eq (list A) instance manually
...
Motivation: make sure we can use it before we define the tactic `mk_dec_eq_instance`.
2017-12-11 16:27:03 -08:00
Sebastian Ullrich
205fbd8136
chore(.gitattributes): use union merge strategy for doc/changes.md
...
No more changelog merge conflicts \o/
2017-12-11 12:49:10 +01:00
Leonardo de Moura
f1510a82c7
chore(tests/lean): fix tests
2017-12-10 19:30:43 -08:00
Leonardo de Moura
d44996e034
feat(library/init/meta): propagate tag information
2017-12-10 19:15:41 -08:00
Leonardo de Moura
e23db3970a
feat(library/init/meta/tactic): apply tactic return parameter name associated with new metavars
2017-12-10 12:11:58 -08:00
Leonardo de Moura
41cfa1bf63
feat(library/init/meta/tactic): induction tactic returns constructor/param names
2017-12-10 09:46:39 -08:00
Leonardo de Moura
c65376d71c
chore(library/constructions/brec_on): suffix _1 is not needed when naming brec_on functional param
...
Reason: we removed support for mutually inductive datatypes from the
kernel.
This change is relevant for the new goal tagging feature.
2017-12-10 09:37:12 -08:00
Leonardo de Moura
8577fe6984
fix(library/init/meta/interactive): induction ... generalizing ... bug
2017-12-10 08:57:25 -08:00
Leonardo de Moura
f288205cce
feat(library/tactic): goal tagging
2017-12-09 16:29:03 -08:00
Leonardo de Moura
24d5a1592d
fix(library/init): add simp lemmas for auto_param and opt_param
2017-12-09 09:59:00 -08:00
Leonardo de Moura
ef784ce7b8
fix(library/tactic/simp_lemmas): auto_params when adding simp lemmas
2017-12-09 09:47:39 -08:00
Leonardo de Moura
623ff2454b
chore(library/init/meta/interactive): remove TODO
...
We now have `whnf_ginductive`
2017-12-08 11:47:20 -08:00
Leonardo de Moura
49e7a642c3
feat(library/init/meta/interactive): merge ginduction and induction
...
This commit is based on 638b34b16de6443.
The changes were applied manually to make sure all changes are
compatible with our plans to `induction`.
2017-12-07 19:10:10 -08:00
Leonardo de Moura
103598bbe0
chore(library/data/rbtree/insert): use weak_trichotomous as an eliminator
2017-12-07 17:40:52 -08:00
Leonardo de Moura
9fff5ff710
chore(tests/lean/run): fix tests
2017-12-06 16:04:24 -08:00
Leonardo de Moura
c5ed881c59
chore(library/data/rbtree/insert): reduce number of cases using custom elimination principle for balance1/balance2
2017-12-06 15:57:44 -08:00
Leonardo de Moura
5ddab48b1e
chore(library/data/rbtree/basic): cleanup
2017-12-06 13:25:07 -08:00
