Leonardo de Moura
|
8ffadce4ab
|
feat(frontends/lean): add "premise" and "premises" command
It is just an alternative notation for "variable" and "variables"
closes #429
|
2015-02-11 18:46:03 -08:00 |
|
Leonardo de Moura
|
30d20e8029
|
chore(frontends/lean/parser): remove dead code
|
2015-02-11 16:29:58 -08:00 |
|
Leonardo de Moura
|
04e92e1e96
|
feat(frontends/lean/parser): reject explicit universe levels in variables and parameters
This modification was motivated by issue #427
|
2015-02-11 16:25:06 -08:00 |
|
Leonardo de Moura
|
a35cce38b3
|
feat(frontends/lean): new semantics for "protected" declarations
closes #426
|
2015-02-11 14:09:25 -08:00 |
|
Leonardo de Moura
|
eceed03044
|
feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command
|
2015-02-11 11:02:59 -08:00 |
|
Leonardo de Moura
|
93f04f3034
|
feat(emacs): update syntax highlight
|
2015-02-11 10:35:38 -08:00 |
|
Leonardo de Moura
|
1832fb6f54
|
feat(*): uniform metaclass names, metaclass validation at 'open' command
|
2015-02-11 10:35:04 -08:00 |
|
Leonardo de Moura
|
9d1cd073c5
|
feat(frontends/lean): add 'print metaclasses' command
|
2015-02-11 10:13:20 -08:00 |
|
Leonardo de Moura
|
2cbaf1bbe3
|
feat(library/scoped_ext): add get_metaclasses API
|
2015-02-11 10:12:28 -08:00 |
|
Leonardo de Moura
|
60fca7575c
|
fix(frontends/lean/pp): bugs when pretty printing abbreviations
|
2015-02-10 19:06:09 -08:00 |
|
Leonardo de Moura
|
9398b887cc
|
fix(library/abbreviation): missing condition
|
2015-02-10 18:34:45 -08:00 |
|
Leonardo de Moura
|
bd304e1911
|
chore(*): style
|
2015-02-10 18:31:17 -08:00 |
|
Leonardo de Moura
|
f9832fb89f
|
test(tests/lean/abbrev1): add test for abbreviation command
|
2015-02-10 18:28:48 -08:00 |
|
Leonardo de Moura
|
43f849bf95
|
feat(frontends/lean/pp): add support for abbreviations in the pretty printer
closes #365
|
2015-02-10 18:27:02 -08:00 |
|
Leonardo de Moura
|
13748b9347
|
feat(library/abbreviation): simplify expand_abbreviations
|
2015-02-10 18:26:39 -08:00 |
|
Leonardo de Moura
|
373d4ca4c6
|
feat(emacs/lean-syntax): highlight 'abbreviation' command
|
2015-02-10 18:22:03 -08:00 |
|
Leonardo de Moura
|
f47e1bed01
|
feat(library/abbreviation): store inverse map ignoring universe level parameters
|
2015-02-10 18:21:32 -08:00 |
|
Leonardo de Moura
|
0d96b6b4cb
|
feat(library/expr_lt): add expression comparison operator that ignores treat level parameters as wildcards
|
2015-02-10 18:20:10 -08:00 |
|
Leonardo de Moura
|
565cd835af
|
feat(frontends/lean): add 'abbreviation' command
|
2015-02-10 17:31:40 -08:00 |
|
Leonardo de Moura
|
64ac3fa4ee
|
feat(library): add 'abbreviation' management module
|
2015-02-10 17:25:11 -08:00 |
|
Leonardo de Moura
|
014271da8b
|
feat(frontends/lean): better error messages for ill-terminated declarations
|
2015-02-10 14:38:00 -08:00 |
|
Leonardo de Moura
|
c3e7b1f817
|
fix(bin/linja.in): problems on Python 3.4 for Windows
|
2015-02-09 18:25:31 -08:00 |
|
Leonardo de Moura
|
daa9bb70b7
|
fix(bin/linja): bug that only happens when uisng linja on Windows
|
2015-02-09 16:42:34 -08:00 |
|
Leonardo de Moura
|
c7ee831c69
|
refactor(library/algebra/ordered_group): use rewrite tactic at ordered_group
|
2015-02-08 17:35:28 -08:00 |
|
Leonardo de Moura
|
f9ff4ee6bd
|
refactor(library/algebra/ring): use rewrite tactic at ring module
|
2015-02-08 17:35:01 -08:00 |
|
Leonardo de Moura
|
058377c8c6
|
feat(library/tactic/rewrite_tactic): treat iff.refl as trivial step in the rewrite tactic
|
2015-02-08 17:27:59 -08:00 |
|
Leonardo de Moura
|
666f697d24
|
fix(frontends/lean/builtin_exprs): 'using' expression should make local constant available for tactics
|
2015-02-08 17:27:22 -08:00 |
|
Leonardo de Moura
|
fcd67649ed
|
refactor(kernel): expose may_reduce_later method
|
2015-02-07 20:36:26 -08:00 |
|
Leonardo de Moura
|
b57f93bad5
|
refactor(kernel): remove unnecessary procedures
|
2015-02-07 20:14:19 -08:00 |
|
Leonardo de Moura
|
1bdf7ae55a
|
feat(kernel/default_converter): make norm_ext virtual
|
2015-02-07 19:25:56 -08:00 |
|
Leonardo de Moura
|
4c2277fccf
|
feat(kernel/converter): more cleanup
|
2015-02-07 19:19:01 -08:00 |
|
Leonardo de Moura
|
73acaca21e
|
refactor(kernel/default_converter): remove extra_opaque_pred
|
2015-02-07 19:05:46 -08:00 |
|
Leonardo de Moura
|
a11d1efb42
|
refactor(kernel/converter): remove mk_default_converter procedures
|
2015-02-07 19:03:58 -08:00 |
|
Leonardo de Moura
|
a47615009f
|
refactor(kernel/type_checker): replace mk_default_converter with default_converter
|
2015-02-07 19:01:59 -08:00 |
|
Leonardo de Moura
|
f018fdabb9
|
refactor(library/kernel_bindings): remove unnecessary procedure
|
2015-02-07 18:57:46 -08:00 |
|
Leonardo de Moura
|
1640568f6a
|
refactor(library/reducible): use default_converter in reducible, and converters based on reducible hints
|
2015-02-07 17:31:53 -08:00 |
|
Leonardo de Moura
|
7823905fc1
|
fix(kernel/default_converter): use is_opaque at is_delta
|
2015-02-07 17:30:36 -08:00 |
|
Leonardo de Moura
|
b4f1029318
|
refactor(library/reducible): define opaque_type_checker using default_converter
|
2015-02-07 17:05:29 -08:00 |
|
Leonardo de Moura
|
e04250f0d8
|
refactor(library/tactic/rewrite_tactic): use default_converter
|
2015-02-07 16:44:51 -08:00 |
|
Leonardo de Moura
|
c04c0e8381
|
refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation
|
2015-02-07 15:19:41 -08:00 |
|
Leonardo de Moura
|
7945b8adab
|
refactor(kernel/type_checker): remove useless procedures
|
2015-02-07 14:55:36 -08:00 |
|
Leonardo de Moura
|
12d320fa19
|
refactor(kernel/default_converter): avoid carrying type_checker and delayed_justification around in the default_converter
|
2015-02-07 14:10:56 -08:00 |
|
Leonardo de Moura
|
71b9215a70
|
refactor(kernel/default_converter): cleanup
|
2015-02-07 13:49:42 -08:00 |
|
Leonardo de Moura
|
3f06f7b6fd
|
refactor(kernel): move default_converter to its own module
|
2015-02-07 11:33:37 -08:00 |
|
Leonardo de Moura
|
d143b525f7
|
feat(library/algebra/ordered_group): reduce compilation time
|
2015-02-06 18:34:41 -08:00 |
|
Leonardo de Moura
|
0f34f4d4a1
|
fix(hott): adjust library to new apply tactic semantics
|
2015-02-06 17:27:56 -08:00 |
|
Leonardo de Moura
|
c2a296b1de
|
feat(library/tactic/apply_tactic): add flag for disabling class instance resolution in the apply tactic
|
2015-02-06 17:27:24 -08:00 |
|
Leonardo de Moura
|
1557a579ed
|
feat(library/tactic/proof_state): add report_failure flag to proof state
tactic can use the flag to produce nice error messages
|
2015-02-06 16:29:04 -08:00 |
|
Leonardo de Moura
|
2126b8ec9a
|
feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic
closes #360
|
2015-02-06 16:14:03 -08:00 |
|
Leonardo de Moura
|
18808d133e
|
refactor(library/tactic/goal): move goal => local_context conversion to goal class
|
2015-02-06 16:09:59 -08:00 |
|