Leonardo de Moura
|
5313cd3467
|
fix(library/init/meta/pos): missing file
|
2018-08-28 07:41:41 -07:00 |
|
Leonardo de Moura
|
805e45bba5
|
chore(tests/shell): fix test
|
2018-08-27 17:54:43 -07:00 |
|
Leonardo de Moura
|
776c977742
|
refactor(kernel): continue constant_info/declaration refactoring
|
2018-08-27 17:23:26 -07:00 |
|
Leonardo de Moura
|
96ff6b1718
|
feat(util/object_ref): add helper functions
|
2018-08-27 16:28:37 -07:00 |
|
Leonardo de Moura
|
3f5db74ab4
|
refactor(library/init/lean/declaration): rename declaration_val ==> constant_val
It doesn't make sense to call it `declaration_val` anymore.
|
2018-08-27 16:07:38 -07:00 |
|
Leonardo de Moura
|
ae18cee0ea
|
chore(library/module): remove pos_info tracking
We will use a completely different approach in Lean4
|
2018-08-27 15:55:57 -07:00 |
|
Leonardo de Moura
|
2ab2265d22
|
chore(library/module): remove dead APIs
|
2018-08-27 15:40:20 -07:00 |
|
Leonardo de Moura
|
dec166b387
|
chore(library/module): remove dead info
|
2018-08-27 15:35:10 -07:00 |
|
Leonardo de Moura
|
d27a360912
|
chore(library/update_declaration): remove dead file
|
2018-08-27 15:18:23 -07:00 |
|
Leonardo de Moura
|
27ef29a50f
|
refactor(kernel/declaration): continue constant_info/declaration refactoring
|
2018-08-27 13:22:10 -07:00 |
|
Leonardo de Moura
|
7bf032d6fe
|
chore(frontends/lean): remove calc-expression
|
2018-08-27 12:20:54 -07:00 |
|
Leonardo de Moura
|
66adac6af6
|
chore(library/init): avoid calc at corelib
|
2018-08-27 12:17:30 -07:00 |
|
Leonardo de Moura
|
4917ab0c65
|
chore(library): remove congr_lemma
|
2018-08-23 16:48:43 -07:00 |
|
Leonardo de Moura
|
e0f7fa3bd9
|
chore(library/tactic): remove leftovers
|
2018-08-23 16:00:34 -07:00 |
|
Leonardo de Moura
|
d334bb1fa7
|
chore(*): remove more stuff
|
2018-08-23 15:56:31 -07:00 |
|
Leonardo de Moura
|
17ae59b5b0
|
chore(*): remove more stuff
|
2018-08-23 15:27:12 -07:00 |
|
Leonardo de Moura
|
c21555240a
|
chore(library/tactic): remove more stuff
|
2018-08-23 15:20:07 -07:00 |
|
Leonardo de Moura
|
646cdfdf40
|
chore(library/init/meta): remove well_founded_tactics
|
2018-08-23 15:14:22 -07:00 |
|
Leonardo de Moura
|
5f65b3a6f1
|
chore(library/tactic): remove unused bindings
|
2018-08-23 15:04:23 -07:00 |
|
Leonardo de Moura
|
e2b912237d
|
chore(library/native_compiler): remove leftovers
|
2018-08-23 14:58:57 -07:00 |
|
Leonardo de Moura
|
a7f6d1d38d
|
chore(library/tactic): remove tactic/eval.cpp and tactic/gexpr.cpp
|
2018-08-23 14:54:41 -07:00 |
|
Leonardo de Moura
|
22101a2c55
|
chore(library/tactic): remove assert_tactic and change_tactic
|
2018-08-23 14:50:55 -07:00 |
|
Leonardo de Moura
|
05a6d8a791
|
chore(library/tactic): remove destruct_tactic, generalize_tactic and fun_info_tactics
|
2018-08-23 14:47:51 -07:00 |
|
Leonardo de Moura
|
8434f43146
|
chore(library/init/meta): remove interactive.lean
|
2018-08-23 14:41:47 -07:00 |
|
Leonardo de Moura
|
973eb89e40
|
chore(library/init/meta/lean): remove old parser support
|
2018-08-23 14:39:10 -07:00 |
|
Leonardo de Moura
|
d405e54a6f
|
chore(library/init/meta/tactic): reduce tactic.lean
|
2018-08-23 14:37:40 -07:00 |
|
Leonardo de Moura
|
ed5d884d8f
|
chore(library/tactic): remove app_builder_tactics
|
2018-08-23 14:22:00 -07:00 |
|
Leonardo de Moura
|
a6604dcf56
|
chore(library/tactic): remove rewrite and apply and interactive tactics
|
2018-08-23 14:18:16 -07:00 |
|
Leonardo de Moura
|
7a47406c4c
|
chore(library/tactic): remove simp_lemmas
|
2018-08-23 14:10:36 -07:00 |
|
Leonardo de Moura
|
88c8c560a9
|
chore(library/equations_compiler): do not generate equation lemmas
|
2018-08-23 14:04:37 -07:00 |
|
Leonardo de Moura
|
3abcd0c9e8
|
chore(frontends/lean/elaborator): remove invoke_tactic
|
2018-08-23 13:49:47 -07:00 |
|
Leonardo de Moura
|
69734dfb3a
|
chore(tests/lean): fix tests
|
2018-08-23 13:49:07 -07:00 |
|
Leonardo de Moura
|
e5c3f04937
|
chore(frontends/lean): remove tactic notation
|
2018-08-23 13:44:52 -07:00 |
|
Leonardo de Moura
|
d27ef3d3b0
|
chore(frontends/lean/builtin_cmds): remove tactic framework dependency
|
2018-08-23 13:34:38 -07:00 |
|
Leonardo de Moura
|
d0f6bbdf02
|
chore(tests/lean): replace run_cmd with #eval
|
2018-08-23 13:32:25 -07:00 |
|
Leonardo de Moura
|
a1fffb2c9d
|
chore(tests/lean/fail/run_command): obsolete test
|
2018-08-23 13:30:07 -07:00 |
|
Leonardo de Moura
|
22ba0a1155
|
chore(library): remove inverse.cpp
We used this module to implement inductive_compiler pack/unpack functions
|
2018-08-23 13:16:27 -07:00 |
|
Leonardo de Moura
|
8e351d46a1
|
chore(library/equations_compiler): remove support for pack/unpack
We don't need it anymore because we removed inductive_compiler/nested.cpp
|
2018-08-23 13:16:27 -07:00 |
|
Leonardo de Moura
|
7fb763c50f
|
chore(library/tactic): remove dsimp and unfold tactics
|
2018-08-23 11:57:38 -07:00 |
|
Leonardo de Moura
|
a10e81e6a6
|
chore(frontends/lean/elaborator): remove unfold tactic dependency
|
2018-08-23 11:57:38 -07:00 |
|
Leonardo de Moura
|
ef27df8907
|
chore(library/tactic): remove simp
|
2018-08-23 11:57:38 -07:00 |
|
Leonardo de Moura
|
9b4f59e511
|
chore(library/inductive_compiler): remove simp references
|
2018-08-23 11:57:38 -07:00 |
|
Leonardo de Moura
|
fc96c335fb
|
chore(library/constructions): remove has_sizeof
This will be implemented in Lean in the future.
|
2018-08-23 11:57:38 -07:00 |
|
Leonardo de Moura
|
dc479c6837
|
chore(library/inductive_compiler): remove mutual.cpp
|
2018-08-23 11:57:38 -07:00 |
|
Sebastian Ullrich
|
fd1aa589cf
|
chore(tests/lean/reader1): fix test
|
2018-08-23 11:03:40 -07:00 |
|
Leonardo de Moura
|
c7cf75508d
|
feat(init/control/coroutine): avoid mutual inductive
Reason: we want to delete the inductive compiler.
|
2018-08-23 10:49:40 -07:00 |
|
Leonardo de Moura
|
252a017445
|
chore(library/inductive_compiler): remove nested.cpp
We added a temporary hack in the old inductive datatype module: we
accept nested inductive declarations.
|
2018-08-23 10:49:40 -07:00 |
|
Sebastian Ullrich
|
5c066b6e84
|
fix(library/derive_attribute): pass options to type_context
|
2018-08-23 10:48:38 -07:00 |
|
Sebastian Ullrich
|
61f8ebf4ef
|
refactor(library/init/lean/parser/reader): destructure reader into monad and has_tokens typeclass
|
2018-08-23 10:38:59 -07:00 |
|
Sebastian Ullrich
|
adfc8c9e62
|
chore(tests/lean/run/deriv): fix test
|
2018-08-23 10:38:59 -07:00 |
|