michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
3630 commits 3 branches 0 tags 28 MiB
Commit graph

3630 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Leonardo de Moura
428d5cfb99 chore(util/sexpr/options): typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 21:20:01 -07:00
Leonardo de Moura
0465c6ef53 fix(frontends/lean): flyinfo for identifiers defined in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 21:15:02 -07:00
Leonardo de Moura
3795d466c1 fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 20:57:24 -07:00
Leonardo de Moura
0c9317b167 feat(frontends/lean/elaborator): add flyinfo for placeholders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 20:25:06 -07:00
Leonardo de Moura
8bd36dabce refactor(kernel/pos_info_provider): get_pos_info return none if position is not available 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 20:17:26 -07:00
Leonardo de Moura
df57043861 fix(frontends/lean/scanner): decode utf8 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 19:58:02 -07:00
Leonardo de Moura
4b604521a0 fix(frontends/lean): add hack for flycheck 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 16:26:04 -07:00
Leonardo de Moura
288831dc66 fix(kernel/formatter): fixes #21 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 15:07:01 -07:00
Leonardo de Moura
bd766d8b0e fix(frontends/lean/elaborator): remove duplicate entries in flyinfo data 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 14:40:26 -07:00
Leonardo de Moura
4cb8fb20fe fix(frontends/lean/elaborator): bug when mixing string and non-strict implict arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:58:20 -07:00
Leonardo de Moura
01908c4dac chore(tests/lean): add 'expensive' file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:35:32 -07:00
Soonho Kong
3cb9b4c265 fix(library/Makefile.common): make OSX-compatible 2014-08-01 10:21:40 -07:00
Leonardo de Moura
d27c85e30c fix(library/Makefile.common): avoid error message when .d files do not exist 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:11:01 -07:00
Leonardo de Moura
fe7ed20058 chore(*): add license badge 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:58:40 -07:00
Leonardo de Moura
8e6324185a fix(tests/lean): adjust tests to new library structure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:37:23 -07:00
Leonardo de Moura
f75beb8087 fix(library/standard/data/list/basic): remove 'sorry' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:15:30 -07:00
Jeremy Avigad
b2c2d1dd44 refactor(library/standard): organize files into a hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
fbaf8b7e77 refactor(library/standard): begin reorganization into hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
df84c4c2ca refactor(library/standard): clean up logic, reorder arguments to elim rules 2014-08-01 09:11:51 -07:00
Jeremy Avigad
c89c96b913 feat(library/standard/list.lean): add facts about lists 2014-08-01 09:11:51 -07:00
Jeremy Avigad
e846c8c76b index on master: 9dc1baa feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
5847743573 feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
8ea5dad4c0 feat(library/standard/congruence.lean): add class to infer that a function is a congruence with respect to two relations 2014-08-01 09:11:51 -07:00
Jeremy Avigad
09d5d074ec feat(library/standard/list.lean): begin to port lists from lean 0.1 2014-08-01 09:11:51 -07:00
Leonardo de Moura
b279c94037 feat(build): cread .d (dependency) files for .lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:08:16 -07:00
Leonardo de Moura
466dd11d1b fix(frontends/lean/dependencies): warning message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 19:59:05 -07:00
Leonardo de Moura
f39b2eb70f feat(frontends/lean): add --flyinfo option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 19:54:21 -07:00
Leonardo de Moura
c01b4bd636 fix(frontends/lean/parser): generate flycheck-friendly import error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 19:03:54 -07:00
Leonardo de Moura
6ca80b5000 feat(frontends/lean): add 'sorry' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 18:35:57 -07:00
Leonardo de Moura
9cf93c8299 feat(library/error_handling): add helpers classes for creating WARNING and INFO annotations for flycheck 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 17:41:39 -07:00
Leonardo de Moura
d5d2c1d069 fix(emacs): syntax highlight issues reported by Jeremy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:49:19 -07:00
Leonardo de Moura
ba98634a7a feat(frontends/lean/pp): do not display metavariable arguments by default, add option pp.metavar_args to control whether they are displayed or not 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:46:16 -07:00
Leonardo de Moura
de05c041c7 feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:46:16 -07:00
Leonardo de Moura
f57fc33442 fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:46:16 -07:00
Soonho Kong
9dfa1b6c1d chore(CMakeLists.txt): replace "lib1;lib2" with "lib1" "lib2" 2014-07-31 14:31:19 -07:00
Soonho Kong
b4c2234e10 chore(shell/CMakeLists.txt): put EXECUTABLE_SUFFIX to lean 2014-07-31 14:11:59 -07:00
Leonardo de Moura
92e90fbd07 feat(library/error_handling): add flycheck_scope helper class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 12:45:54 -07:00
Leonardo de Moura
1a8a2b0811 refactor(library/unifier): process_flex_rigid method before adding yet another case split 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 12:25:35 -07:00
Leonardo de Moura
8e222e6244 fix(kernel/converter): missing constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 12:25:35 -07:00
Soonho Kong
14a406d4d7 feat: add "--flycheck" option to print out error msgs for flycheck 2014-07-31 11:18:51 -07:00