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 |
|
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
|
a66a08c89e
|
feat(frontends/lean): parse strings as expressions of type 'string.string'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 10:00:55 -07:00 |
|
Leonardo de Moura
|
8b8881deae
|
fix(util/hash): relax pre-condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 09:56:50 -07:00 |
|
Leonardo de Moura
|
f464775af6
|
fix(frontends/lean/parser): bug when parsing identifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 08:36:25 -07:00 |
|
Leonardo de Moura
|
9f9f93645b
|
feat(library/standard): add bit, char, and string types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 08:36:05 -07:00 |
|
Leonardo de Moura
|
0198dfc7c5
|
feat(frontends/lean): parse numerals as expressions of type 'num.num'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 08:09:33 -07:00 |
|
Leonardo de Moura
|
7593ee1468
|
refactor(library/standard): remove parameter from 'tactic' inductive type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 08:09:24 -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 |
|