Leonardo de Moura
|
8e9f97e95e
|
fix(frontends/lean): do not save identifier info
|
2014-10-29 17:38:59 -07:00 |
|
Leonardo de Moura
|
83e4c0fcec
|
feat(frontends/lean): hide tactic "types"
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
|
2014-10-28 22:38:10 -07:00 |
|
Leonardo de Moura
|
f3fdc70400
|
refactor(library/tactic): add auxiliary module 'library/tactic/elaborate'
|
2014-10-23 10:26:11 -07:00 |
|
Leonardo de Moura
|
7c62446023
|
refactor(frontends/lean): remove dead code
|
2014-10-22 17:39:06 -07:00 |
|
Leonardo de Moura
|
e95c7c5f70
|
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-10-22 17:29:50 -07:00 |
|
Leonardo de Moura
|
5e15ac0c92
|
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
|
2014-10-22 17:29:50 -07:00 |
|
Leonardo de Moura
|
7c617955d0
|
refactor(library/tactic): move 'exact' tactic to separate module
|
2014-10-22 17:29:44 -07:00 |
|
Leonardo de Moura
|
53a64ac767
|
refactor(library/tactic): move intros_tactic initialization to intros_tactic module
|
2014-10-20 17:47:52 -07:00 |
|
Leonardo de Moura
|
3c4419ff23
|
refactor(library/tactic): move rename_tactic to separate module
|
2014-10-20 17:41:40 -07:00 |
|
Leonardo de Moura
|
ac9397816f
|
refactor(library/tactic): move apply_tactic initialization to apply_tactic module
|
2014-10-20 17:32:32 -07:00 |
|
Leonardo de Moura
|
7d0100a340
|
feat(library/tactic): add 'intros' tactic
|
2014-10-20 15:26:16 -07:00 |
|
Leonardo de Moura
|
e6606ef2ac
|
feat(library/tactic): add 'rename' hypothesis tactic
|
2014-10-14 18:19:34 -07:00 |
|
Leonardo de Moura
|
58c9421bab
|
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70
|
2014-10-14 17:18:40 -07:00 |
|
Leonardo de Moura
|
516c0c73b9
|
refactor(*): remove dependency to thread_local C++11 keyword, the
current compilers have several bugs associated with it
We use the simpler __thread (gcc and clang) and
__declspec(thread) (visual studio).
|
2014-09-24 12:51:04 -07:00 |
|
Leonardo de Moura
|
b6781711b1
|
refactor(*): explicit initialization/finalization for serialization
modules, expression annotations, and tactics
|
2014-09-22 15:26:41 -07:00 |
|
Leonardo de Moura
|
364bba2129
|
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:26:36 -07:00 |
|
Leonardo de Moura
|
2869d9059f
|
feat(frontends/lean): change 'proof-qed' semantics: no backtracking
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-12 17:40:30 -07:00 |
|
Leonardo de Moura
|
e3ab0a1d10
|
feat(frontends/lean): improve error messages when users forget to import 'tactic'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 08:33:29 -07:00 |
|
Leonardo de Moura
|
6b8b5f3dd8
|
feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 08:06:28 -07:00 |
|
Leonardo de Moura
|
a7d660f875
|
feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 20:45:10 -07:00 |
|
Leonardo de Moura
|
5527955ba8
|
feat(frontends/lean): add 'proof-qed' notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 19:30:48 -07:00 |
|
Leonardo de Moura
|
138267b53a
|
feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 18:58:32 -07:00 |
|
Leonardo de Moura
|
ee531ec0e2
|
feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 14:09:01 -07:00 |
|
Leonardo de Moura
|
6ab46396d8
|
feat(library/tactic): expose 'trace' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 10:52:45 -07:00 |
|
Leonardo de Moura
|
e1d909455c
|
refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 10:45:09 -07:00 |
|
Leonardo de Moura
|
b2b76b078f
|
feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-01 20:43:53 -07:00 |
|
Leonardo de Moura
|
cbac21ec7f
|
feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-01 19:05:22 -07:00 |
|