max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
12940 commits 1 branch 0 tags 5.3 GiB
Commit graph

1894 commits

Author SHA1 Message Date
Gabriel Ebner
0c15724e8e fix(library/tactic/simplify): handle universe polymorphic simplification rules 
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not.  Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
 2017-08-03 17:42:07 +01:00
Leonardo de Moura
b6c691cead test(tests/lean/run/whnf_mvar): add test to check whether whnf instantiate mvars or not 
@digama0 As I suspected, `whnf` already instantiates metavariables.
 2017-08-03 11:29:22 +01:00
Gabriel Ebner
22011dcde4 chore(init/algebra/order): typo 
Thanks to @fpvandoorn for proof-reading!
 2017-08-02 15:41:51 +01:00
Leonardo de Moura
fdaa26f2fd feat(library/equations_compiler/wf_rec): fixes #1782 2017-08-02 15:12:04 +01:00
Gabriel Ebner
5922f71c50 feat(library/init/algebra/order): add default value for lt 2017-08-02 14:41:35 +01:00
Gabriel Ebner
ce509e621a refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
Sebastian Ullrich
4f66673fc2 feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers 2017-08-02 14:32:39 +01:00
Leonardo de Moura
39fa7625b8 feat(library/init/meta/interactive): add specialize tactic 
closes #1779
 2017-08-02 10:20:25 +01:00
Gabriel Ebner
c15f2979c6 fix(frontends/lean/util): allow docstrings after variables 2017-08-01 10:18:05 +01:00
Mario Carneiro
f369e34bd6 chore(library/standard): remove standard.lean (unused, and confusing given stdlib) 2017-07-28 16:47:53 +01:00
Leonardo de Moura
870ce5c0fe fix(library/init/meta/constructor_tactic): fixes #1771 2017-07-28 09:45:51 +01:00
Leonardo de Moura
58016bc037 chore(tests/lean): fix test suite 2017-07-26 14:10:02 +01:00
Mario Carneiro
4dc261393f refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
Mario Carneiro
09f9cada65 chore(init/data/nat): rename add_one_eq_succ -> add_one 2017-07-26 11:52:10 +01:00
Mario Carneiro
cc81118892 refactor(init/data): move out some nat lemmas 2017-07-26 11:52:10 +01:00
Mario Carneiro
7d4fe55bff fix(tests/lean/run/choice_anon_ctor): fix test 2017-07-26 11:52:10 +01:00
Mario Carneiro
74aeb250ec refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
Leonardo de Moura
c7c8387bd8 chore(tests/lean/run/bin_tree): fix broken test 2017-07-21 05:05:42 -07:00
Leonardo de Moura
4faae27069 perf(frontends/lean): add notation #[...] 
The new notation should be use to input long sequences.
Closes #1755
 2017-07-21 04:20:48 -07:00
Mario Carneiro
97a01d25fd fix(init/meta/tactic): skip solved goals in seq_focus and seq 
and all/any_goals. This occurs when solving the first subgoal generated by `tac1; tac2` closes the second goal as well, before the second `tac2` invocation is run. Reported by @jldodds on gitter.
 2017-07-21 02:10:48 -07:00
Sebastian Ullrich
ae5bc52d97 fix(frontends/lean/elaborator): pass expected type through visit_function 2017-07-20 01:58:29 -07:00
Sebastian Ullrich
9ed72acabe fix(frontends/lean/builtin_exprs): allow constant patterns in do notation 2017-07-20 01:51:00 -07:00
Sebastian Ullrich
7d39b3e948 refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax 2017-07-20 01:51:00 -07:00
Gabriel Ebner
3392aa90b5 fix(frontends/lean/definition_cmds): support parameters in mutual defs 2017-07-13 15:14:46 +01:00
Gabriel Ebner
ecf7e3d2d8 feat(tests): test overriden VM functions on small values 2017-07-11 23:00:09 +01:00
Gabriel Ebner
8f31cff99b chore(tests): move 1723 test to the expected output tests 2017-07-09 08:05:05 +02:00
Josh Pollock
ee55a03205 fix(src/library/vm,tests/lean): fixes #1723 2017-07-09 08:05:05 +02:00
Leonardo de Moura
8dcccd3bfc fix(frontends/lean/parser): make sure imax and max level arguments are parsed using the same precendence we use to parse application arguments 
This commit addresses an issue raised by @digama0 on the Lean slack channel.
 2017-07-07 12:43:07 -07:00
Leonardo de Moura
9555a104d6 feat(library/init/meta/tactic): simplify ‹p› notation 
@jroesch See the new test :)
 2017-07-07 12:05:02 -07:00
Sebastian Ullrich
ac8de2472e feat(library/tactic/induction_tactic): clear hypothesis before introducing new ones 2017-07-07 10:06:30 -07:00
Leonardo de Moura
91f4fd9507 fix(library/equations_compiler/elim_match): undo bcf44f7 
See issue #1739

Main problem with this commit: the counter-examples for non-exhaustive matches will be
cryptic when using nested inductive types.
 2017-07-07 09:16:07 -07:00
Leonardo de Moura
ced4b6a54d fix(library/init/meta/interactive): fixes #1733 2017-07-06 22:34:24 -07:00
Leonardo de Moura
0cfb48c095 fix(library/equations_compiler/util): PR #1731 2017-07-06 21:29:23 -07:00
Sebastian Ullrich
c209cdc8be fix(kernel/inductive/inductive): identify indices modulo whnf 2017-07-06 20:59:58 -07:00
Sebastian Ullrich
d386e65775 fix(library/equations_compiler/util): noequation: guess arity modulo whnf 2017-07-06 20:59:58 -07:00
Leonardo de Moura
514c1e30c9 fix(library/tactic/dsimplify): issue reported by @semorrison at gitter 
`dsimp` option `unfold_reducible` was not working correctly.
 2017-07-05 21:48:44 -07:00
Leonardo de Moura
cfab344bcc fix(library/delayed_abstraction): fixes #1728 2017-07-05 17:10:18 -07:00
Leonardo de Moura
1bc9af53f2 fix(library/init/meta/simp_tactic): fixes #1724 2017-07-05 11:59:23 -07:00
Leonardo de Moura
bb9e3ddae2 feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 
@Armael: this change may affect your project.

The file `doc/changes.md` explains the motivation for the change.
 2017-07-05 11:42:55 -07:00
Sebastian Ullrich
30f4b2f2dd refactor(library): list.taken/dropn ~> list.take/drop 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
f024ccd75d refactor(frontends/lean/token_table,library): take ~> assume 2017-07-05 11:20:10 -07:00
Sebastian Ullrich
f95f70fe56 feat(frontends/lean/builtin_exprs): support have ... := ... in term mode 2017-07-05 11:20:10 -07:00
Leonardo de Moura
dd3616dd16 feat(library/init/meta/interactive): simp_all ==> simp * at * 
cc @Kha
 2017-07-04 11:57:16 -07:00
Leonardo de Moura
44c901bf11 fix(library/init/meta/interactive): make sure all input hypotheses are simplified before we clear the old ones 
The new test exposes the bug.
The bug is similar to the one at `simp [h] at *` described at issue #1675
 2017-07-03 21:58:55 -07:00
Leonardo de Moura
b86847ec72 fix(library/init/logic): mark eq.substr with [elab_as_eliminator] 
See issue #1718
 2017-07-03 17:27:41 -07:00
Leonardo de Moura
e24f3341d4 feat(library/init/meta/interactive): simp without foo ==> simp [-foo] 
This commit also adds "exception" validation.
A bad "exception" was being silently ignored.
We can also exclude hypotheses. Example: `simp [*, -h]`
 2017-07-03 17:10:46 -07:00
Leonardo de Moura
76799db032 feat(library/init/meta/interactive): simph ==> simp [*] 
This modification was suggested by @kha.

TODO:
- Use `simp [-f]` instead of `simp without f`
- Allow users to remove hypothesis from `*`. Example: `simp [*, -h]`
  for simplify using all hypotheses but `h`.
 2017-07-03 15:14:47 -07:00
Leonardo de Moura
6b3e28d30b feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 
This complete addresses the two pending items at 16711fcdba
 2017-07-03 13:28:46 -07:00
Leonardo de Moura
9a41f0f899 fix(library/init/meta/tactic): by_cases tactic 
Before this commit, the `by_cases p` tactic would synthesize
`inst : decidable p` type class resolution, and then use the
`cases` tactic (dependent elimination). This would create
problems since occurrences of `inst` would be replaced with
`decidable.is_true h` in one branch, and `decidable.is_false h` in the
other. Where `h`s (we have two of them, one for each branch) are
fresh hypotheses introduced by the `cases` tactic.
For example, assume we have the term in our goal.

        `@ite p inst A a b`

This term would become

        `@ite p (decidable.is_true h) A a b` (in the first branch where `h : p`)

and
        `@ite p (decidable.is_false h) A a b` (in the second where `h : not p`)

Now, suppose we try to executed the following tactic in the first branch

        `rw [if_pos h]`

it will fail since `if_pos h` is actually `@if_pos p inst h`, and
we will not be able to unify

        `@ite p (decidable.is_true h) A a b =?= @ite p inst ?A ?a ?b`

This commit workarounds this problem by applying cases on
`@decidable.em p inst : p or not p` instead of `inst : decidable p`.
Thus, the term `inst` is not replaced with `decidable.is_true h` and
`decidable.is_false h`.

The new test `tests/lean/run/simp_dif.lean` demonstrates the problem above.
 2017-07-02 21:34:10 -07:00
Leonardo de Moura
16711fcdba feat(library/tactic/dsimplify): new configuration options for dsimp 
TODO for `dsimp`:
- Add an option for reducing [reducible] definitions
- Add (to_unfold : list name) similar to the one in the `simp` tactic
 2017-07-02 18:26:03 -07:00