Daniel Selsam
f3e71e52fc
feat(frontends/smt2/parser.cpp): allow tracing from the smt tactic
2017-03-12 09:54:09 -07:00
Daniel Selsam
aa209d89e7
fix(library/smt/prove.lean): collect_props was collecting (H : Prop)
2017-03-12 09:54:01 -07:00
Daniel Selsam
06233c32c2
perf(constructions/injective): avoid unnecessary app-builder invocation
2017-03-12 09:53:18 -07:00
Simon Hudon
58b9d0ae8e
feat(library/data/bitvec): to_nat and of_nat cancel each other
2017-03-12 09:38:57 -07:00
Simon Hudon
b6889e91fe
feat(lib/init/data/nat): add function pow and a Galois connection between div and mul
2017-03-12 09:38:19 -07:00
Leonardo de Moura
c694dbd600
fix(frontends/lean/elaborator): conflict between (: t :) and (::) notations
...
It was preventing us from using `(::)`
2017-03-12 09:29:42 -07:00
Daniel Selsam
89d0f1773e
chore(tests/lean/inductive_resultant_level_inferrence): update expected output
2017-03-11 18:46:55 -08:00
Leonardo de Moura
d37fd17725
fix(kernel/level): potential compiler specific behavior
2017-03-11 18:30:28 -08:00
Daniel Selsam
cdc24bae77
feat(library/constructions/injective): do not include propositions
2017-03-11 18:12:43 -08:00
Leonardo de Moura
95c93e7211
feat(library/constructions/no_confusion): do not include propositions
2017-03-11 17:36:04 -08:00
Leonardo de Moura
9c24b81cbf
feat(frontends/lean/elaborator): improve error message
2017-03-11 16:35:40 -08:00
Leonardo de Moura
d352ac4bcb
chore(tests/lean): fix tests
2017-03-11 12:20:42 -08:00
Leonardo de Moura
740d42ea45
fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom
2017-03-11 12:20:39 -08:00
Leonardo de Moura
ab1a92ac3b
feat(tmp/micro_lenses): experiment with van Laarhoven-style lens
2017-03-11 11:35:02 -08:00
Leonardo de Moura
3a4cd38ba9
chore(library/init): remove reducible annotations for id, const, etc, and move $ notation to core.lean
2017-03-11 11:34:16 -08:00
Leonardo de Moura
2f6c4d91e4
feat(library/init/core): simplify proofs
2017-03-10 22:42:21 -08:00
Daniel Selsam
e72d516252
refactor(inductive_compiler): use subst to prove packs injective instead of constructors
2017-03-10 22:27:29 -08:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08:00
Leonardo de Moura
98e93b73b2
feat(library/init/meta/name): add name.replace_prefix
2017-03-10 22:16:21 -08:00
Leonardo de Moura
300f6b2344
chore(tmp/micro_lenses): update
2017-03-10 18:42:15 -08:00
Sebastian Ullrich
e3bfd90b06
fix(frontends/lean/elaborator): default recover_from_error to false for most commands
...
Fixes #1446
fix(frontends/lean/util): quoting private name
uncovered by now failing run test
2017-03-09 20:51:35 -08:00
Leonardo de Moura
1b48d51cdd
fix(emacs/lean-syntax): new transient commands
2017-03-09 20:41:35 -08:00
Sebastian Ullrich
16558bf082
refactor(library,library): rename pre_monad to has_bind
2017-03-09 20:32:25 -08:00
Sebastian Ullrich
04f1d114a3
chore(script/gen_constants_cpp): make it run from anywhere
2017-03-09 20:30:03 -08:00
Sebastian Ullrich
763097dbd2
refactor(library): revise the monadic hierarchy
2017-03-09 20:30:03 -08:00
Leonardo de Moura
b0a33259ee
fix(library/compiler/simp_inductive): array^.data should not be treated as a regular projection
2017-03-09 19:11:51 -08:00
Leonardo de Moura
6916a8ceca
fix(library/compiler/inliner): inliner was unfolding constants aggressively when trying to reduce projections
...
@digama0 After this commit, your example will also produce a
non-destructive update.
```lean
structure test :=
(data1 : array nat 3)
(data2 : array nat 3)
(sz: nat)
def test.write (s : test) (i : fin 3) (v : nat) :=
{s with data1 := s^.data1^.write i v, data2 := s^.data2^.write i v}
set_option trace.array.update true
(fin.of_nat 1) 10 in
(a^.data1^.read (fin.of_nat 1), a^.data2^.read (fin.of_nat 2)) -- destructive write
```
2017-03-09 18:52:27 -08:00
Leonardo de Moura
9d3c0497cb
chore(frontends/lean): rename transient commands
...
See issue #1432
2017-03-09 18:41:19 -08:00
Leonardo de Moura
a00f2e49a7
chore(frontends/lean): remove several command aliases
...
We still have many more to remove and rename.
See issue #1432
2017-03-09 16:49:03 -08:00
Leonardo de Moura
e875141322
feat(library/tactic/intro_tactic): make sure unused names are used if the user did not provide them
2017-03-09 16:03:18 -08:00
Leonardo de Moura
3e757d890a
feat(library/tactic/intro_tactic): allow '_' in interactive mode as the anonymous name for intros, cases, induction
2017-03-09 15:42:36 -08:00
Leonardo de Moura
b6f6126075
feat(frontends/lean/pp): add attribute [pp_using_anonymous_constructor] for marking structures we should use the anonymous constructor notation when pretty printing instances
2017-03-09 15:17:18 -08:00
Leonardo de Moura
c58f61e925
feat(frontends/lean/elaborator): new encoding for structure updates {s with ...}
...
See discussion at #1438
https://github.com/leanprover/lean/pull/1438#discussion_r105007325
@digama0 With this commit, the original `array_list.write` will also
perform a destructive update when the reference counter for `l` is 1.
```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α :=
λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v }
```
2017-03-09 00:11:51 -08:00
Leonardo de Moura
77f8479457
feat(library/type_context): allow zeta during type class resolution and app_builder
2017-03-08 23:04:56 -08:00
Leonardo de Moura
c086c58b4a
fix(library/init/meta/simp_tactic): simp_intro_aux tactic should not fail when hypothesis cannot be simplified
2017-03-08 21:20:43 -08:00
Leonardo de Moura
8979663164
feat(library/tactic/simplify): relax reducibility constraints when matching implicit arguments
...
Motivation: if the explicit part matches (what the user sees), then the implicit part must morally match too.
If it doesn't because of reducibility setting, the behavior is usually counterintuitive.
2017-03-08 20:08:54 -08:00
Leonardo de Moura
4ab0a6d8d2
fix(library): problems with the subtype constructor and field renaming
...
The problem was not detected by the test suite because of issue #1446
2017-03-08 19:42:12 -08:00
Jeremy Avigad
666ca36470
fix(library/tests/lean/*): fix tests
2017-03-08 19:31:27 -08:00
Jeremy Avigad
37f3e5cc69
refactor(library/data/dlist): change 'inv' to 'invariant'
2017-03-08 19:31:27 -08:00
Jeremy Avigad
95f75bbbee
refactor(library/init/data/subtype/basic): rename subtype constructor and projections
2017-03-08 19:31:27 -08:00
Leonardo de Moura
d775ee98b4
feat(frontends/lean): auto_param support at structure_instance, and better error messages
...
Summary:
- A field value was being elaborated more than once when there is
another field whose default value depends on it.
The new test `structure_default_value_issue.lean` exposes the problem.
- Better error message and localization at field type mismatches.
When there is field type mismatch, the error message contains the
field name, and the error is reported at the field position instead of
`{`.
- We add support for auto_param at structure instances `{...}`
See #1422
2017-03-08 18:04:36 -08:00
Leonardo de Moura
23935ee390
feat(frontends/lean): allow auto_param notation in structure declarations
...
See #1422
TODO: take the auto_param into account in the `{ ... }` notation.
2017-03-08 15:41:30 -08:00
Leonardo de Moura
ceeb77ec8c
fix(library/compiler/erase_irrelevant): erase types of irrelevant lambdas
...
This modification makes sure we do not create unnecessary closures,
and avoid artificial dependencies that may prevent destructive updates.
2017-03-08 14:48:45 -08:00
Leonardo de Moura
7a99d87cbd
fix(library/tactic/ac_tactics): allow nested ac_app macros in perm_ac macro
...
fixes #1442
2017-03-08 13:46:49 -08:00
Sebastian Ullrich
970e11bf5e
feat(frontends/lean/{elaborator,structure_cmd}): allow overriding field defaults
2017-03-08 10:41:20 -08:00
Sebastian Ullrich
b3887f21a4
fix(shell/server): remove unnecessary dependencies of info_task and use intermediate envs
2017-03-08 10:40:59 -08:00
Daniel Selsam
42e08cac36
chore(tests/lean/run/1430.lean): repro for #1430
2017-03-07 20:12:07 -08:00
Leonardo de Moura
7ac6b14d2a
chore(library/init/data/int/basic): use abstract when transfering in an instance declaration
...
@johoelzl I'm using `abstract` tactic because instances are
automatically marked as [reducible], and they will be unfolded when
solving unification constraints. This cannot be avoided since we need to
solve unification constraints such as
int.has_add =?= comm_ring.to_has_add int.comm_ring
The `abstract tac` tactic creates an auxiliary lemma to store the proof
generated by `tac`. If we use `print int.comm_ring` we can see that
the definition is much smaller. The proofs are irrelevant. So, this has
no drawbacks, and gives us a good performance boost.
2017-03-07 19:57:43 -08:00
Leonardo de Moura
1ac240e2db
chore(tests/lean): fix tests
2017-03-07 19:45:00 -08:00
Johannes Hölzl
d6eae3265c
feat(library/data/dlist): setup transfer for dlist
2017-03-07 19:30:51 -08:00
