Leonardo de Moura
4595c50f7e
fix(library/hop_match): in locally bound variable management
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065
refactor(*): error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3
feat(frontends/lean): improve error message for expressions containing unsolved metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 13:21:44 -08:00
Leonardo de Moura
12451e4a35
feat(frontends/lean/pp): display implicit arguments when expression contains metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 12:42:05 -08:00
Leonardo de Moura
d83a13d044
doc(doc/lean/tutorial): update tutorial
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 21:56:08 -08:00
Leonardo de Moura
84f017f127
chore(tests/lua): use default environment instead of creating a new one
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:24:04 -08:00
Leonardo de Moura
35bacf95fc
feat(shell): provide the default environment when parsing Lua files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:21:14 -08:00
Leonardo de Moura
7f818ecd92
feat(library): match procedure for higher-order patterns
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:45:24 -08:00
Leonardo de Moura
e6c322d97f
feat(kernel/free_vars): make free_vars module functions more robust
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:44:28 -08:00
Leonardo de Moura
29fec3fecc
fix(builtin/util): bug incorrect encoding of \t and \n in regular expression, and missing local
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:40:41 -08:00
Leonardo de Moura
915644f3b3
fix(util/debug): avoid infinite loop when Ctrl-D is pressed after an assertion violation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:20:35 -08:00
Leonardo de Moura
5d9a95addd
refactor(kernel/free_vars): replace max_free_var with relaxed free_var_range
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:06:57 -08:00
Leonardo de Moura
582569b793
feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 16:46:53 -08:00
Leonardo de Moura
4d9eb4ac6c
feat(kernel): add max_free_var function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 16:45:34 -08:00
Leonardo de Moura
f2cac0410e
doc(examples/lean): new examples
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 20:21:16 -08:00
Leonardo de Moura
6508e63a17
feat(builtin/macros): add assume/take macros for making proof scripts more readable
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 18:36:37 -08:00
Leonardo de Moura
781720a26a
feat(builtin/kernel): add left_comm theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 18:08:08 -08:00
Leonardo de Moura
a1a467a65f
refactor(builtin): move congruence theorems to kernel/if_then_else modules
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 13:48:28 -08:00
Leonardo de Moura
a0a92f11b7
feat(builtin/congr): add congruence theorems for contextual simplification
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 13:37:36 -08:00
Leonardo de Moura
53537d0684
feat(builtin/kernel): 'implication' simplification theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 13:35:20 -08:00
Leonardo de Moura
50f281b430
feat(builtin/kernel): add eqf_intro and eqf_elim theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 11:13:54 -08:00
Leonardo de Moura
4057f0d2fe
feat(emacs): minor improvements to emacs mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-11 11:13:20 -08:00
Leonardo de Moura
745c702ffb
fix(build): dependency problem on some platforms
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-10 19:06:15 -08:00
Leonardo de Moura
d4a7d796a5
feat(builtin): prove strong induction theorem, add < theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-10 18:46:33 -08:00
Leonardo de Moura
5fb718c03a
fix(build): broken dependencies between lean executable and .olean, *_decls.cpp and *_decls.h files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-10 10:58:35 -08:00
Leonardo de Moura
9e8b083673
feat(emacs): more highlighting
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 20:44:01 -08:00
Leonardo de Moura
b85b45b40f
test(tests/lean): When and Cond tactical tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 20:43:39 -08:00
Leonardo de Moura
3008cad151
feat(emacs): highlight tactics
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 20:10:57 -08:00
Leonardo de Moura
2cf73fc4d2
feat(emacs): useful abbreviations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 19:57:00 -08:00
Leonardo de Moura
65bdb9c7e0
fix(frontends/lean): unprotected call to Lua API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 19:56:20 -08:00
Leonardo de Moura
411f14415d
feat(builtin): automatically generate Lean/C++ interface for builtin theories
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 18:09:53 -08:00
Leonardo de Moura
a339a53f50
feat(util/options): 'verbose' as a system option, add -q (quiet) option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 15:31:58 -08:00
Leonardo de Moura
8c41b4e899
feat(build): run tests using -t
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 14:12:32 -08:00
Leonardo de Moura
2179e57db3
refactor(builtin): move if_then_else to its own module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 14:08:39 -08:00
Leonardo de Moura
52e11dbbee
test(tests/lean): 'using' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:21:14 -08:00
Leonardo de Moura
fdeb457a81
feat(kernel/pos_info_provider): add support for file names in pos_info_provider
...
The idea is to include the file name when displaying justification objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:19:30 -08:00
Leonardo de Moura
dff0b9011b
chore(builtin/cast): cleanup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:06:22 -08:00
Leonardo de Moura
3e18cdfeec
feat(util/format): do not use colors by default
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:56:58 -08:00
Leonardo de Moura
6fe362ef07
feat(emacs): include lean-mode Emacs files in the distribution
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:50:07 -08:00
Leonardo de Moura
7a1ee92507
feat(emacs): add short-cuts \C-c\C-l and \C-c\C-x to execute Lean files in Emacs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:45:31 -08:00
Leonardo de Moura
84e211b81b
fix(frontends/lean): missing ':' in error messages
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4
feat(frontends/lean): include filename in error messages, use GNU error message style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:01:27 -08:00
Leonardo de Moura
bcfd043a06
feat(emacs): add basic indentation support
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 09:48:18 -08:00
Leonardo de Moura
b30d524418
feat(emacs): add input method based on Agda's input method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 09:32:47 -08:00
Leonardo de Moura
87b238efcd
chore(builtin/kernel): cleanup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 09:00:05 -08:00
Leonardo de Moura
57c0006916
chore(*): cleanup lean builtin symbols, replace :: with _
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
25086947fa
fix(builtin/kernel): incorrect comment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 19:14:11 -08:00
Leonardo de Moura
e42b616438
fix(kernel/normalizer): equality between semantic attachments
...
Given a heterogenous equality: a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 19:10:30 -08:00
Leonardo de Moura
8e9d88c2cf
refactor(builtin/kernel): prove iff::intro, and add a new name for it boolext (Boolean extensionality)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 18:31:45 -08:00
Leonardo de Moura
a4b3d6d6c8
refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 17:25:14 -08:00