Daniel Selsam
03ed74fea1
fix(inductive_compiler): generate has_sizeof for structures
2016-10-05 15:10:21 -07:00
Leonardo de Moura
cf00d266de
fix(CMakeLists.txt): disable check when compiling with emscripten
2016-10-05 15:05:22 -07:00
Leonardo de Moura
a52ea72c62
fix(library/vm/vm_environment): invalid vm_obj being returned
2016-10-05 15:05:22 -07:00
Leonardo de Moura
73ed9db161
chore(frontends/lean/token_table): remove old keyword
2016-10-05 08:46:23 -07:00
Leonardo de Moura
7f30844348
feat(library/tactic/simplifier/simp_lemmas): add tactic for applying one simplification step form a simp_lemmas set
2016-10-04 19:51:33 -07:00
Leonardo de Moura
4516d1b046
feat(library/init/meta/attribute, library/tactic/user_attribute): make sure caching_user_attribute is in (Type 1)
2016-10-04 02:05:34 -07:00
Leonardo de Moura
6b582ca6c3
fix(library/vm/vm): bug at get_constant
2016-10-04 01:58:39 -07:00
Leonardo de Moura
bd4c77d414
fix(library/tactic/user_attribute): anonymous attribute names are now allowed
2016-10-04 01:11:33 -07:00
Leonardo de Moura
545b89d556
fix(library/vm): memory violation
2016-10-04 00:09:52 -07:00
Leonardo de Moura
269fb198fb
perf(library/type_context): process function before arguments
2016-10-03 23:34:14 -07:00
Gabriel Ebner
837938981e
fix(tests/util/lp): fix debug build
2016-10-03 22:22:12 -07:00
Soonho Kong
8b1f55010b
feat(CMakeLists.txt): include cpp14_lang/sized_deallocation.cmake
...
Previously, it downloaded cpp14_lang/sized_deallocation.cmake file from
Github during cmake was running. This worked in most cases but failed in an
environment where network connection was not provided. A particular
example is to build Ubuntu packages. See [1] for details.
This patch is to include cpp14_lang/sized_deallocation.cmake file in the
repository. It also set COMP_CMAKE_PATH to indicate the location of the
pre-downloaded file. 'CACHE INTERNAL ""' is required to set the scope of
COMP_CMAKE_PATH file so that it's visible inside of
'CompBase.cmake'. See [2] for details.
[1]: https://launchpadlibrarian.net/263258156/buildlog_ubuntu-precise-amd64.lean_0.2.0.20160603023524.gitc73b2860d5211187e9aa1039d1a49dcabdca4292~12.04_BUILDING.txt.gz
[2]: https://cmake.org/cmake/help/v2.8.12/cmake.html#command:set
2016-10-03 22:21:55 -07:00
Gabriel Ebner
93cf15391c
fix(library/tactic/simplifier/util): fix deserialization of flat macros
2016-10-03 22:20:15 -07:00
Leonardo de Moura
2164b4d553
feat(kernel/type_checker): make sure anonymous binder names are rejected by the kernel
2016-10-03 22:15:49 -07:00
Leonardo de Moura
629cfa6ba1
feat(library/tactic/simplifier): disable broken theory_simplifiers
2016-10-03 22:06:44 -07:00
Leonardo de Moura
d549044d27
feat(library/init/meta,library/tactic/simplifier): user defined simp attributes
2016-10-03 21:39:17 -07:00
Leonardo de Moura
4ee9554c96
fix(library/vm/vm): reference may be invalidated when the vector is resized
2016-10-03 21:31:17 -07:00
Leonardo de Moura
a0a7e22bb7
fix(library/vm/vm): uninitialized variable
2016-10-03 21:25:30 -07:00
Leonardo de Moura
88c6177a4c
fix(library/tactic/simplifier/simp_lemmas): incorrect binding
2016-10-03 20:46:22 -07:00
Leonardo de Moura
7be74a6c0c
feat(library/init/meta/simp_tactic): add command for creating simp attributes
2016-10-03 20:38:15 -07:00
Leonardo de Moura
d252f4ac7d
feat(frontends/lean/elaborator): improve mini-lenses
2016-10-03 20:17:45 -07:00
Leonardo de Moura
e9ef7d1342
chore(util/parray): remove dead code
2016-10-03 19:09:57 -07:00
Leonardo de Moura
4a2946f5dd
feat(library/tactic/eval): eval_expr for arbitrary expressions
2016-10-03 19:01:22 -07:00
Leonardo de Moura
16985d0de1
feat(frontends/lean/elaborator): better error message for eval_expr
2016-10-03 18:23:47 -07:00
Leonardo de Moura
12eb886f49
refactor(library/vm/vm): remove parray
2016-10-03 17:26:03 -07:00
Leonardo de Moura
e6fbbbbc2d
feat(util/rb_map): add unsigned_map
2016-10-03 16:26:58 -07:00
Leonardo de Moura
7465529445
feat(library/tactic): 'eval_expr' tactic skeleton
2016-10-03 16:26:28 -07:00
Leonardo de Moura
ee9ba1e5cb
feat(library/init/meta/simp_tactic): add tactic for adding universe polymorphic lemma to simp set
2016-10-03 14:41:36 -07:00
Leonardo de Moura
7c07d269f9
refactor(library/tactic/user_attribute): cache builder must be a tactic
2016-10-03 14:20:37 -07:00
Leonardo de Moura
7e5a4483a6
feat(library/reducible): get_reducibility_fingerprint
2016-10-03 13:31:59 -07:00
Leonardo de Moura
1baa953b48
feat(frontends/lean/elaborator): improve error localization
2016-10-02 13:33:49 -07:00
Leonardo de Moura
838b3329ce
fix(frontends/lean/elaborator): structure instance update with type classes
2016-10-02 11:36:22 -07:00
Leonardo de Moura
872360db0f
feat(util/hash): use #if
2016-10-02 10:46:11 -07:00
Leonardo de Moura
ee3c857c88
fix(util/hash): 32-bit version
2016-10-02 10:03:04 -07:00
Leonardo de Moura
f21f1219d9
fix(frontends/lean/structure_cmd): handle is_one_placeholder
2016-10-02 08:07:19 -07:00
Leonardo de Moura
4f69fe943a
fix(frontends/lean/structure_cmd): make sure structure_cmd takes the option default_priority into account
2016-10-01 13:47:19 -07:00
Leonardo de Moura
9631b70295
fix(library/class): attributes instance and class were not being registered in the attribute_manager when procedures add_instance and add_class were being used directly
2016-10-01 13:45:23 -07:00
Leonardo de Moura
95ffdca3f7
feat(frontends/lean/decl_attributes): add 'default_priority' attribute
2016-10-01 13:27:08 -07:00
Leonardo de Moura
837915f06b
fix(frontends/lean/builtin_exprs): bug when parsing in quoted names
2016-10-01 13:19:24 -07:00
Leonardo de Moura
7ab12ed57f
feat(library/init/algebra): improve transport_to_additive (copy attributes)
2016-10-01 12:55:17 -07:00
Leonardo de Moura
89703ce669
feat(library/vm/vm_expr): expose replace
2016-10-01 09:23:40 -07:00
Leonardo de Moura
6644748d45
fix(library/vm/vm_declaration): is_theorem implies is_definition
2016-10-01 09:22:45 -07:00
Leonardo de Moura
c0022253a7
feat(frontends/lean/tactic_notation): allow lemmas to be removed
2016-09-30 19:53:51 -07:00
Leonardo de Moura
fd6dc8154a
feat(library/init/meta/interactive): add interactive tactics
2016-09-30 19:02:45 -07:00
Leonardo de Moura
d627011786
feat(frontends/lean/tactic_notation): do is tactic unit in begin end blocks.
2016-09-30 16:35:45 -07:00
Leonardo de Moura
051b6bd026
feat(frontends/lean/tactic_notation): add notation for entering auto-quotation mode
2016-09-30 16:18:52 -07:00
Leonardo de Moura
9ea858e6fe
feat(frontends/lean/tactic_notation): nested interactive tactics
2016-09-30 14:53:07 -07:00
Leonardo de Moura
23ce2b0587
feat(frontends/lean/tactic_notation, library/init/meta/interactive): add "interactive" versions of define/assert/definev/assertv/note tactics
2016-09-29 18:48:32 -07:00
Leonardo de Moura
572751c56e
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
...
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
2016-09-29 17:56:35 -07:00
Sebastian Ullrich
515da8bbb7
fix(emacs): don't pass --lean option
2016-09-29 15:29:19 -07:00
