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
Johannes Hölzl
9d62638e9a
chore(library/init/meta/transfer): short documentation of transfer rules
2017-03-07 19:30:51 -08:00
Johannes Hölzl
1f45995c16
feat(library/init/meta/transfer): add transfer and use for int
...
This commit introduces the transfer method. As application it is
used it to prove that the integers form a commutative ring.
2017-03-07 19:30:51 -08:00
Johannes Hölzl
ca0fe37c41
feat(library/init/meta/tactic): add mk_local_pis
2017-03-07 19:30:51 -08:00
Johannes Hölzl
da4f552a7a
feat(library/init/meta): add decidable_eq for binder_info
2017-03-07 19:30:51 -08:00
Johannes Hölzl
69ed20f656
feat(library/init/meta/match_tactic): add tactic_format for pattern
2017-03-07 19:30:51 -08:00
Johannes Hölzl
0ad5f5bc89
feat(library/init/meta/expr): add instantiate_local(s)
2017-03-07 19:30:51 -08:00
Johannes Hölzl
9e9b289031
feat(library/init/data/prod): add prod.map
2017-03-07 19:30:51 -08:00
Johannes Hölzl
b593d090f2
feat(library/init/data/list): add remove_all
2017-03-07 19:30:51 -08:00
Johannes Hölzl
1c30a593c1
feat(library/init/data/list): add enum
2017-03-07 19:30:51 -08:00
Johannes Hölzl
16aaa9b88e
feat(library/init/data/list): add unzip
2017-03-07 19:30:51 -08:00
Johannes Hölzl
4c88e2c5b0
feat(library/init/data/int): use relators for proof of int is a ring
2017-03-07 19:30:51 -08:00
Leonardo de Moura
8530e39375
fix(library/tactic/smt/congruence_closure): fixes #1430
...
@dselsam I did not include your repro in the test suite because it will not work after we
enforce the `is_inner_ginductive_ir` check.
2017-03-07 17:13:29 -08:00
Leonardo de Moura
8d3c7e7180
fix(frontends/lean/builtin_exprs): fixes #1433
2017-03-07 16:21:12 -08:00
Leonardo de Moura
839645c489
feat(library/system/io): replace io.monad with io.bind, io.return and io.map
2017-03-07 16:10:47 -08:00
Leonardo de Moura
0c6108ce7a
chore(library/init/data/quot): use Sort instead of Type
...
Remark: The kernel was already using Sort. So, the limitation was
artificial. Moreover, it may seem unnecessary to have quotients of
proofs in a proof irrelevant system, but this is useful for proving
a more general funext lemma. This more general version is needed in
the new tested contributed by @digama0.
2017-03-07 14:29:57 -08:00
Leonardo de Moura
b69e2006f5
chore(kernel/quotient/quotient): update comments
...
The comments were written before the Type => Sort change
2017-03-07 14:11:51 -08:00
Mario Carneiro
793017b190
feat(library/init/logic.lean): add Sort -> Prop universe lift
2017-03-07 14:01:59 -08:00
Leonardo de Moura
51958df84b
chore(frontends/lean/token_table): remove dead keywords
2017-03-07 14:00:49 -08:00
Leonardo de Moura
c427350dc0
chore(frontends/lean/token_table): remove dead commands
2017-03-07 13:50:14 -08:00
Daniel Selsam
7dcc36277a
feat(frontends/lean/inductive_cmds.cpp): better resultant universe inference
2017-03-07 12:55:01 -08:00
Leonardo de Moura
bc01593639
chore(tmp/micro_lenses): better set for lenses.compose
2017-03-07 11:58:11 -08:00
Leonardo de Moura
cf2db32cf3
feat(tmp/micro_lenses): better definition that supports destructive updates
2017-03-07 11:18:31 -08:00
Leonardo de Moura
943576b8e9
feat(library/compiler/extract_values): restrict extra_values to nat/int/char/string/name
2017-03-07 11:14:32 -08:00
Leonardo de Moura
9a263a2766
chore(library/init): instances are reducible and are inlined by the compiler
...
So, these instances would create two copies of `p` after inlining
2017-03-07 10:58:09 -08:00
Leonardo de Moura
faeac14ed7
feat(library/parray): add trace option for tracking destructive updates
2017-03-07 10:57:40 -08:00
Leonardo de Moura
09c70a7e03
chore(tmp/micro_lenses): experiment for RFC
2017-03-07 09:44:10 -08:00
Leonardo de Moura
425b5ffc11
chore(library/data/dlist): make local notation less cryptic
2017-03-06 18:09:32 -08:00
Leonardo de Moura
0d6d52004b
feat(library/data/dlist): difference lists
2017-03-06 17:23:26 -08:00
Leonardo de Moura
f2faea9b9f
refactor(frontends/lean/equations_validator): move validation code to another file
2017-03-06 14:36:42 -08:00
Daniel Selsam
4330e733c5
feat(inductive_compiler): API for is_ginductive_inner_*
2017-03-06 14:01:59 -08:00
Daniel Selsam
5f0ebf90de
fix(frontends/lean/structure_cmd): call inductive compiler without params in type
2017-03-06 14:01:46 -08:00
Daniel Selsam
d122f4417a
chore(src/library/print): update to use Sort
2017-03-06 14:01:33 -08:00
Leonardo de Moura
1d71103f29
feat(library/tactic/cases_tactic): add support for generalized inductive datatypes at 'cases' tactic
2017-03-06 11:49:04 -08:00
Sebastian Ullrich
2394f1faa5
fix(frontends/lean/util): do not fall back to current position
2017-03-06 11:02:51 -08:00
Sebastian Ullrich
c4ebfab14c
fix(frontends/lean/structure_cmd): inheriting defaulted field depending on field starting with implicit parameter
2017-03-06 11:02:51 -08:00
Sebastian Ullrich
87b98d5aa2
fix(frontends/lean/structure_cmd): fix assertion violation when field depends on defaulted field
2017-03-06 11:02:50 -08:00
Sebastian Ullrich
e5018ee4f8
chore(bin/lean-gdb): fix macro pretty-printing
2017-03-06 11:02:50 -08:00
Jeremy Avigad
803e1958fa
refactor(library/init/classical.lean): move definition of some
2017-03-06 10:54:42 -08:00
Daniel Selsam
ce1ec69ea6
fix(frontends/lean/decl_utils.cpp): closes #1417
2017-03-06 10:54:22 -08:00
Daniel Selsam
d461cb001e
feat(inductive_compiler): get_ginductive_num_indices
2017-03-06 10:53:58 -08:00
Leonardo de Moura
4608782669
fix(init/logic): eq.mpr and eq.mp can be use for type casting
...
So, they should be `def`. Otherwise code generation will fail.
2017-03-06 09:13:39 -08:00
Leonardo de Moura
045fe4ad25
fix(frontends/lean/structure_cmd): allow default values for function fields
2017-03-06 07:41:42 -08:00
Leonardo de Moura
156e5603d6
feat(library/init/category/combinators): put list combinators in the namespace list
...
In this way we can use them with the ^. notation
2017-03-05 21:30:30 -08:00
