Leonardo de Moura
bbc4380a52
fix(library/unifier): bug exposed by recent changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 19:02:30 -07:00
Leonardo de Moura
069f217215
fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 17:21:21 -07:00
Leonardo de Moura
d14cbfd7e9
refactor(frontends/lean/elaborator): local context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 16:25:54 -07:00
Leonardo de Moura
9cc2015caa
feat(library/unifier): better error message for invalid local context
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5
feat(library/match): add 'local' backtracking
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51
feat(library/match): add basic match_plugin that just invokes whnf before failing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 08:37:03 -07:00
Soonho Kong
a4b023a175
feat(bin/lmake): support multiple targets; add '-C', '-f' options
2014-08-05 02:19:15 -07:00
Leonardo de Moura
56d151ef7f
feat(frontends/lean): 'partial' aliases. closes #24
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 22:08:10 -07:00
Leonardo de Moura
f4031b620f
feat(library/match): extend match_plugin interface, and allow them to recursively invoke the matcher
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 18:30:30 -07:00
Leonardo de Moura
c34c2f4f5c
feat(library/match): match universe levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 18:30:30 -07:00
Leonardo de Moura
b0a5ff7f93
refactor(library): rename hop_match to match
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 18:30:30 -07:00
Soonho Kong
57410e7818
fix(bin/lmake): use '-j' option for make
...
[skip ci]
2014-08-04 17:28:57 -07:00
Leonardo de Moura
0d5e346143
fix(library/expr_lt): make sure the builtin order is AC-compatible
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 15:51:10 -07:00
Soonho Kong
b2cb49fa1f
feat(bin/lmake): add lmake
...
lmake tries to find a makefile in the current working-directory or its
ancestors and invoke the makefile if found. If a makefile is not found,
it calls lean directly. This is also used for flycheck-lean.
Usage:
$ lmake
$ lmake all
$ lmake clean
$ lmake basic
$ lmake basic.lean
$ lmake /home/user/projects/lean/library/.../basic.lean
$ lmake --flyinfo --flycheck basic
2014-08-04 15:17:23 -07:00
Leonardo de Moura
b9fadeb86e
fix(util/realpath): realpath on cygwin
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 15:06:08 -07:00
Leonardo de Moura
5755ce4bfc
fix(util/lean_path): use unix style paths when using cygwin
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 14:45:23 -07:00
Leonardo de Moura
53c7124c2b
fix(util/realpath): rename realpath to lrealpath
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 14:42:44 -07:00
Leonardo de Moura
bc4cef9ecb
feat(build): clean-olean target deletes .olean and .d files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 14:01:13 -07:00
Leonardo de Moura
59f6cb5962
fix(build): delete incorrect/old .d and .olean files, detect errors when generating .d files.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 13:58:48 -07:00
Leonardo de Moura
d5bb7d45ec
fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 13:58:47 -07:00
Leonardo de Moura
47d49643b0
feat(library/standard/logic/connectives/if): add more general if_congr theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 13:58:47 -07:00
Soonho Kong
d8ae285f93
fix(library/Makefile.common): clean remove olean/d files recursively
...
[skip ci]
2014-08-04 11:47:24 -07:00
Leonardo de Moura
94efd51fc5
chore(library/standard/logic/connectives/if): cleanup
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 23:11:52 -07:00
Leonardo de Moura
c3f57cdb1c
feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 22:58:12 -07:00
Leonardo de Moura
ae2e0fd3dc
feat(library/standard/logic/connectives/if): add 'if-then-else' congruence theorem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 21:41:01 -07:00
Leonardo de Moura
63d478c63f
fix(tests/lua/hop1): incorrect assertion
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 20:06:50 -07:00
Leonardo de Moura
f3cb5f2f84
feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 20:03:49 -07:00
Leonardo de Moura
552be37d48
feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 16:03:58 -07:00
Leonardo de Moura
2dca68e645
chore(util/list): add inline functions for commonly used patterns in list processing code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 13:51:38 -07:00
Leonardo de Moura
5611c6a0a0
chore(util/lean_path): workaround 'spurious' warning produced by g++ in release mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 13:28:05 -07:00
Leonardo de Moura
50b0c17092
feat(library/unifier): add more information in error messages due to type errors when assigning metavariables
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 09:49:30 -07:00
Leonardo de Moura
938b4e8421
test(tests/lean/run): add unicode in identifiers test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 20:05:46 -07:00
Leonardo de Moura
aeebd942f2
refactor(library/standard): use relative paths in some files in the standard library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 20:04:27 -07:00
Leonardo de Moura
bae9700260
fix(frontends/lean/dependencies): take relative paths into account when computing dependencies
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 20:03:51 -07:00
Leonardo de Moura
4b030c5d5f
feat(library/module): relative module path
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 19:47:55 -07:00
Leonardo de Moura
8768197c24
feat(util/lean_path): add dirname and path_append aux functions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 18:12:28 -07:00
Leonardo de Moura
700c911cf7
chore(library/standard/logic/class/decidable): add missing 'end'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 17:00:01 -07:00
Leonardo de Moura
148836d14b
feat(library/standard/data/option): add basic theorems for option types
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 16:59:01 -07:00
Leonardo de Moura
689c1ee58d
chore(README.md): add link to standard library documentation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 15:54:03 -07:00
Leonardo de Moura
8c37a95164
fix(frontends/lean/scanner): typo reported by clang++
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 15:24:04 -07:00
Leonardo de Moura
249c878597
fix(frontends/lean/elaborator): warning message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 15:21:23 -07:00
Leonardo de Moura
fbc4a7af3b
feat(library/unifier): when unifier.expensive == true, then use only restrict higher-order unification (a fragment slightly more general than higher-order pattern matching) for solving class-instance constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 14:30:25 -07:00
Leonardo de Moura
5e2185cfbe
feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 09:14:35 -07:00
Leonardo de Moura
a62e6f84e3
feat(frontends/lean/scanner): allow letter-like unicode characters and sub/super-scripts in identifiers
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 00:47:58 -07:00
Leonardo de Moura
52e3505599
feat(frontends/lean): display warning message when importing file that uses 'sorry'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 00:47:58 -07:00
Leonardo de Moura
53833c70e9
fix(library/coercion): spurious 'replacing coercion', fixes #22
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-01 21:45:37 -07:00
Jeremy Avigad
b832b2e33e
refactor(library/standard/data/nat): stylistic changes
2014-08-01 21:22:54 -07:00
Jeremy Avigad
b5db9a4797
feat(library/standard/data/nat): port most recent nat to lean 0.2
2014-08-01 21:22:53 -07:00
Jeremy Avigad
4b05e70762
feat(library/standard/logic/axioms): add import default
2014-08-01 21:22:53 -07:00
Jeremy Avigad
77931f2af8
feat(library/standard): add markdown documentation
2014-08-01 21:22:53 -07:00