Leonardo de Moura
|
6ea7bb3ea4
|
feat(frontends/lean/builtin_exprs): add 'including' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 18:37:09 -07:00 |
|
Leonardo de Moura
|
8ab0b5bee3
|
feat(frontends/lean/elaborator): use local declarations as class instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 18:18:25 -07:00 |
|
Leonardo de Moura
|
00e1a7db23
|
feat(frontends/lean/elaborator): add class instance elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 15:45:50 -07:00 |
|
Leonardo de Moura
|
079672f6f9
|
feat(frontends/lean): add 'class' and 'instances' infrastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 14:28:09 -07:00 |
|
Leonardo de Moura
|
f1884ee5f9
|
chore(frontends/lean): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 13:22:32 -07:00 |
|
Leonardo de Moura
|
d7cb1952ae
|
feat(kernel): simplify choice_fn, and make its interface closer to the unifier_plugin interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 12:47:33 -07:00 |
|
Leonardo de Moura
|
b94ce412ae
|
fix(library/unifier): non-termination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 10:32:01 -07:00 |
|
Leonardo de Moura
|
a97f82be1a
|
fix(library/standard): orelse notation, avoid conflict with inductive datatype declaration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 10:10:05 -07:00 |
|
Leonardo de Moura
|
e0501104e2
|
feat(library/tactic): add 'fixpoint' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 01:30:28 -07:00 |
|
Leonardo de Moura
|
7fb2b0f6d8
|
feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 22:31:05 -07:00 |
|
Leonardo de Moura
|
ce282a549a
|
feat(frontends/lean): add 'prefix' notation declaration command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 21:37:56 -07:00 |
|
Leonardo de Moura
|
6d773a2ba4
|
fix(library/standard): not notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 21:29:15 -07:00 |
|
Leonardo de Moura
|
855ffcba34
|
feat(library/standard): add pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 20:43:16 -07:00 |
|
Leonardo de Moura
|
110b622b83
|
feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 20:41:51 -07:00 |
|
Leonardo de Moura
|
c854ad3d65
|
refactor(library/unifier): add is_def_eq alias
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 18:01:59 -07:00 |
|
Leonardo de Moura
|
b5f63e78ca
|
feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 17:23:29 -07:00 |
|
Leonardo de Moura
|
fa1857e6a9
|
fix(frontends/lean/notation_cmd): fix default, add 'prev' action
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 16:44:44 -07:00 |
|
Leonardo de Moura
|
9ec4f23522
|
fix(library/standard): congr1 and congr2 theorem definition, we should allow A and B to inhabit different universes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 16:25:14 -07:00 |
|
Leonardo de Moura
|
7d27368708
|
refactor(library/standard): use inductive datatype to define inhabited
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 15:05:19 -07:00 |
|
Leonardo de Moura
|
aba4534acb
|
feat(library/unifier): 'forget' justifications after finding a solution, the justifications are only needed inside the unifier (for implementing nonchronological backtracking)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 14:14:07 -07:00 |
|
Leonardo de Moura
|
a009225435
|
feat(kernel/metavar): expose destructive assign
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 14:07:47 -07:00 |
|
Leonardo de Moura
|
b49902807c
|
refactor(kernel/metavar): separate substitution from their justifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 14:01:22 -07:00 |
|
Leonardo de Moura
|
abbd054b51
|
feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 13:04:46 -07:00 |
|
Leonardo de Moura
|
079592c446
|
feat(library/unifier): eagerly apply substitution to improve quick failure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 12:58:30 -07:00 |
|
Leonardo de Moura
|
db0ef64c04
|
feat(util/lazy_list_fn): handle the 'is_nil' case more efficiently
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 11:29:04 -07:00 |
|
Leonardo de Moura
|
c9cfb844f1
|
feat(library/unifier): add 'quick' failure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 11:28:21 -07:00 |
|
Leonardo de Moura
|
dd96bb151b
|
refactor(library/unifier): reduce the number unify procedure 'flavors'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 11:15:43 -07:00 |
|
Leonardo de Moura
|
d63ccbcf94
|
fix(library/unifier): missing case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 10:51:59 -07:00 |
|
Leonardo de Moura
|
528d51bc57
|
feat(library/standard): add congr theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 09:44:36 -07:00 |
|
Leonardo de Moura
|
0ff145e59b
|
feat(library/tactic): add apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 09:20:01 -07:00 |
|
Leonardo de Moura
|
c1538bfc40
|
test(tests/lean/run): add 'apply subst' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 09:07:56 -07:00 |
|
Leonardo de Moura
|
c9994ca00c
|
feat(library/unifier): when projecting give preference to most recent locals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 09:01:29 -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
|
c3abf81382
|
chore(emacs): update emacs mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 18:37:53 -07:00 |
|
Leonardo de Moura
|
60c637fb9d
|
feat(library/tactic): add 'exact' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 18:37:32 -07:00 |
|
Leonardo de Moura
|
37b5b7c4c2
|
feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 18:10:42 -07:00 |
|
Leonardo de Moura
|
04b2a620f8
|
fix(frontends/lean/elaborator): instantiate metavariables before displaying error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 18:07:11 -07:00 |
|
Leonardo de Moura
|
3809a3cc2c
|
chore(frontends/lean): code cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 17:32:13 -07:00 |
|
Leonardo de Moura
|
181a739a5e
|
feat(frontends/lean/elaborator): report unassigned metavariables as goals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 16:26:06 -07:00 |
|
Leonardo de Moura
|
6a6ebd5c2d
|
refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 15:39:25 -07:00 |
|
Leonardo de Moura
|
d46ade94a7
|
refactor(frontends/lean): remove unnecessary code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 14:47:41 -07:00 |
|
Leonardo de Moura
|
3e1bb96935
|
feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 14:47:18 -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
|
0f27856e4a
|
feat(library/tactic): new apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 13:14:50 -07:00 |
|
Leonardo de Moura
|
cc3fb0c51f
|
feat(util/name_generator): allow name generator to be created without providing any argument in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 12:39:41 -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 |
|