Leonardo de Moura
072fa7ec49
feat(library/data/nat): add aux lemmas
2015-07-02 22:27:21 -07:00
Leonardo de Moura
e33946ff02
feat(library/data/nat/fact): define factorial
2015-07-02 20:25:34 -07:00
Leonardo de Moura
b9114260f8
feat(script/lib_perf): use gtime if time doesn't work
2015-07-02 11:04:16 -07:00
Leonardo de Moura
7de7c5b73d
feat(library/definitional/projection): define projections using auxiliary macro
2015-07-02 10:49:49 -07:00
Leonardo de Moura
c15bcf1354
refactor(library/projection): remove projection macro from library
2015-07-02 08:48:13 -07:00
Leonardo de Moura
dd145926a2
fix(library/coercion): compilation warning
2015-07-02 07:26:00 -07:00
Leonardo de Moura
aa338f6002
test(tests/lean/run): add test showing new coercion module addresses issue #668
2015-07-01 16:41:19 -07:00
Leonardo de Moura
4ae9f3ea81
feat(library/coercion): new coercion manager
...
closes #668
2015-07-01 16:32:34 -07:00
Leonardo de Moura
fe26c37fcb
refactor(library/tc_multigraph): improve tc_multigraph API
2015-07-01 16:01:40 -07:00
Leonardo de Moura
765865ed41
chore(library/tc_multigraph): remove dead code
2015-07-01 15:48:55 -07:00
Leonardo de Moura
d44d576194
refactor(library/coercion): simplify coercion module API
2015-07-01 14:40:12 -07:00
Leonardo de Moura
d5c38777af
refactor(library/coercion): simplify coercion_class
2015-07-01 14:29:23 -07:00
Leonardo de Moura
0f5b7a36f5
chore(library/coercion): remove lua bindings for coercion module
...
Reason: we will refactor the coercion module.
See issue #668
2015-07-01 14:08:49 -07:00
Leonardo de Moura
667f647b27
feat(kernel/expr_eq_fn): add small optimization
2015-07-01 09:19:36 -07:00
Leonardo de Moura
0f64a6e545
feat(library/data/rat/order): use 'trans-instance' to improve performance of migrate command
2015-07-01 08:57:10 -07:00
Leonardo de Moura
14f7e3de94
fix(library/algebra): missing file
2015-06-30 18:15:13 -07:00
Leonardo de Moura
cf574d0127
feat(library): assign priorities to notation declarations in the standard library
...
Now, even if the user opens the namespaces in the "wrong" order, the
notation + coercions will behave as expected.
2015-06-30 17:38:13 -07:00
Leonardo de Moura
cabe30ba71
feat(frontends/lean): allow user to assign priorities to notation declarations
2015-06-30 17:10:27 -07:00
Leonardo de Moura
a1d1a8272a
refactor(frontends/lean): move parse_priority to util
2015-06-30 16:22:52 -07:00
Leonardo de Moura
4ea57196ff
chore(frontends/lean/parser_config): remove dead code
2015-06-30 16:04:00 -07:00
Leonardo de Moura
880f212494
feat(library/class): allow transitive instances that have instances arguments
2015-06-30 14:54:12 -07:00
Leonardo de Moura
9a9e975bc8
feat(frontends/lean/migrate_cmd): ignore derived transitive instances in the migrate command
2015-06-30 14:00:41 -07:00
Leonardo de Moura
d20f831602
feat(library/class): add is_derived_trans_instance predicate
2015-06-30 13:59:02 -07:00
Leonardo de Moura
e7c3c887b6
feat(kernel/type_checker): add 'check' procedure that uses 'opaque_hints'
...
The hints only affect performance. If a declaration type checks assuming
some constants are opaque, it should also type check without this
assumption. Of course, it may be much slower.
2015-06-30 13:12:34 -07:00
Leonardo de Moura
772ed111e5
refactor(kernel): move extra_opaque_converter to kernel, and rename it to hint_converter
2015-06-30 12:59:28 -07:00
Leonardo de Moura
e635d9be9f
refactor(kernel): rename get_weight to get_height at declaration
...
Motivation:
- It is the standard name for the concept: declaration height
- Avoid confusion with the expression weight
2015-06-30 12:59:10 -07:00
Leonardo de Moura
1e6550eda6
feat(kernel/default_converter): take into account the 'theorem' annotations in the converability checker
...
The idea is that we should seldon need to unfold theorems.
The convertability checker should use that.
When the convertability checker was implemented, theorems were opaque in
Lean. So, this hint was not needed.
This modification is another workaround for the performance problem with
the migrate command at library/data/real/division.lean.
This solution is better than applying proof irrelevance eagerly because
it also addresses similar problems in the HoTT library which does not
support proof irrelevance.
This commit also enables the conv_opt for all theorems.
2015-06-30 10:42:26 -07:00
Leonardo de Moura
acc0832928
feat(kernel/default_converter): add "eager" proof irrelevance optimization
2015-06-29 19:10:39 -07:00
Leonardo de Moura
b5444c1314
refactor(frontends/lean/builtin_cmds): allow "constant" edges in the instance transitive closure graph
2015-06-29 18:57:05 -07:00
Leonardo de Moura
9cefe708ee
feat(frontends/lean/builtin_cmds): display derived instances
2015-06-29 11:06:59 -07:00
Jeremy Avigad
e6ce5d9b72
refactor(library/data/fin): put fin.val coercion in fin namespace
2015-06-29 21:24:38 +10:00
Jeremy Avigad
a54fb42f87
refactor(library/data/int/basic): put int.of_nat coercion in int namespace
2015-06-29 21:00:42 +10:00
Jeremy Avigad
130eb3f6d9
fix(library/data/int/basic): change notation from -[n+1] to -[1+n] to avoid conflict e.g. with -[coercions]
2015-06-29 15:23:11 +10:00
Jeremy Avigad
3bf18c174e
feat(library/algebra/ordered_group): define abs in terms of max, make some theorems constructively valid
2015-06-29 15:23:11 +10:00
Jeremy Avigad
b19331f28f
feat(library/data/nat/order): add theorems for max and min
2015-06-29 15:23:11 +10:00
Jeremy Avigad
1a164d8fc9
feat(library/algebra/ordered_group): add theorems for max and min
2015-06-29 15:23:11 +10:00
Jeremy Avigad
70e551c6d6
feat(library/algebra/order,library/data/nat/order,library/*): instantiate nat to lattice, add theorems
2015-06-29 15:23:11 +10:00
Jeremy Avigad
93e5124d71
feat(library/algebra/order): add lattices, min, max
2015-06-29 15:23:11 +10:00
Jeremy Avigad
0d25831111
refactor(library/algebra/order): cleanup, and remove unused class
2015-06-29 15:23:11 +10:00
Leonardo de Moura
0fc2efe88e
fix(library/tactic/rewrite_tactic): fixes #702
2015-06-28 20:37:17 -07:00
Leonardo de Moura
95720b1670
fix(frontends/lean/elaborator): fixes #687
2015-06-28 19:58:57 -07:00
Leonardo de Moura
ecfc01b2d0
test(tests/lean/run): add test for <d notation
...
see issue #695
remark: we have to fix the tutorial the ASCII notation for fold is `<d`
instead of `<D`
2015-06-28 13:10:15 -07:00
Leonardo de Moura
1b864a838f
fix(library/tactic/induction_tactic.cpp): condition for checking whether 'induction' tatic is applicable or not
...
fixes #690
2015-06-28 13:07:02 -07:00
Leonardo de Moura
88844f6261
chore(src/library/user_recursors): add missing include
2015-06-28 12:53:48 -07:00
Leonardo de Moura
2f75768243
feat(library/tactic/rewrite_tactic): fail when nothing is rewritten
...
fixes #686
2015-06-28 12:05:00 -07:00
Leonardo de Moura
d1eaa7bcda
feat(frontends/lean/parse_rewrite_tactic): accept trailing comman in rewrite tactic
...
see issue #695
2015-06-28 11:45:30 -07:00
Leonardo de Moura
4a4ef48344
fix(frontends/lean/parse_rewrite_tactic): fixes #691
2015-06-28 11:28:05 -07:00
Leonardo de Moura
869ad261c5
fix(frontends/lean/elaborator): fixes #689
2015-06-27 16:19:38 -07:00
Leonardo de Moura
52564ecc0f
refactor(library/algebra/group_power): open namespaces in the "right" order
2015-06-27 14:51:00 -07:00
Leonardo de Moura
8616ed096e
fix(library/composition_manager): typo
2015-06-27 14:12:26 -07:00
