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

3449 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
99a1966fd6 refactor(library/standard/set): use the same style for mem_inter and mem_union 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:32:59 -07:00
Leonardo de Moura
88130f339e feat(library/standard): add basic set theory that does not rely on classical axioms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:18:33 -07:00
Leonardo de Moura
3a77226b92 feat(library/standard/bool): add bor_to_or theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:17:55 -07:00
Leonardo de Moura
25f7929ea3 feat(library/standard/bool): add band_assoc and bor_assoc theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:50:57 -07:00
Leonardo de Moura
4b2e403023 test(tests/lean/run): add more tests sent by Cody 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:17:38 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:12:54 -07:00
Leonardo de Moura
83d38674c9 feat(kernel/error_msgs): improve cryptic type mismatch error messages where the types may seem identical because key information is being suppressed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 09:41:25 -07:00
Leonardo de Moura
6ca120bf77 test(tests/lean/run): add Cody's file to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 08:17:46 -07:00
Leonardo de Moura
0cdd4a267c feat(frontends/lean/pp): pretty print 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:56:35 -07:00
Leonardo de Moura
60cc9ac8e2 feat(frontends/lean/pp): pretty print 'have' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:35:26 -07:00
Leonardo de Moura
cf35c07786 fix(frontends/lean): fix 'let' annotation placement and pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:00:22 -07:00
Leonardo de Moura
206206060f test(tests/lean/hott): add some of Vladimir's definitions as tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 20:50:37 -07:00
Leonardo de Moura
8e402ae862 fix(kernel/type_checker): error message position information 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 20:33:44 -07:00
Leonardo de Moura
cb232f2a9b fix(kernel/inductive): use has_expr_metavar_strict instead of has_expr_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:57:54 -07:00
Leonardo de Moura
5c5dea7c8e feat(kernel/expr): add has_expr_metavar_strict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:54:04 -07:00
Leonardo de Moura
d9ee994281 feat(library/hott): copy basic files to hott library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:13:04 -07:00
Leonardo de Moura
5bf3197306 refactor(frontends/lean): create theorem_queue class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 15:00:51 -07:00
Leonardo de Moura
78a1670905 refactor(frontends/lean): cleanup add_delayed_theorem method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 14:01:20 -07:00
Leonardo de Moura
70ef92cd5e feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:53:44 -07:00
Leonardo de Moura
23af5ab217 fix(library/unifier): eager whnf application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:37:02 -07:00
Leonardo de Moura
556861c8d6 fix(library/unifier): remove incorrect assertion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 07:52:10 -07:00
Leonardo de Moura
c1b523d642 feat(util/worker_queue): allow main thread to process tasks while waiting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 23:24:04 -07:00
Leonardo de Moura
3ec30bf537 feat(frontends/lean): add parallel_import option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 22:46:49 -07:00
Leonardo de Moura
709b5ce90f fix(kernel/justification): duplicate position 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:16:49 -07:00
Leonardo de Moura
70c887a0bd fix(library/unifier): fix cryptic error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:10:32 -07:00
Leonardo de Moura
e79b0b11cf test(tests/lean/run): another test for the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 20:55:05 -07:00
Leonardo de Moura
01cec1e1f1 fix(library/unifier): more bugs in the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 20:05:37 -07:00
Leonardo de Moura
cf44c80ffb fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 16:00:38 -07:00
Leonardo de Moura
7b84503133 fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 15:03:57 -07:00
Leonardo de Moura
1c191c1ec7 fix(frontends/lean/elaborator): instantiate assigned metavariables before collecting unassigned ones 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 15:02:33 -07:00
Leonardo de Moura
0f12e5a35b fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 13:49:45 -07:00
Leonardo de Moura
abe1dbd7e0 refactor(library/standard): cleanup notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:36:28 -07:00
Leonardo de Moura
a450ad5a95 feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:24:01 -07:00
Leonardo de Moura
a5b9a7b296 fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:10:45 -07:00
Leonardo de Moura
811f46e97b feat(frontends/lean/pp): add option for displaying internal names associated with private declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:03:54 -07:00
Leonardo de Moura
0c668a31fe fix(frontends/lean/pp): display private 'internal' names in a human readable way 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 10:58:13 -07:00
Leonardo de Moura
cd522ff670 feat(emacs): improve font highlighting in emacs mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 10:54:06 -07:00
Leonardo de Moura
a59eec39b8 feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:44:40 -07:00
Leonardo de Moura
022a151cf7 feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:33:31 -07:00
Leonardo de Moura
21176c61fe fix(tests/lean): move crash.lean to different directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:48:35 -07:00
Leonardo de Moura
736b219e65 fix(frontends/lean/elaborator): pretty print placeholders as '_' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:46:03 -07:00
Leonardo de Moura
e7c7d5718a fix(frontends/lean/pp): fix bug in the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:30:30 -07:00
Leonardo de Moura
15c1e39f88 feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:43:40 -07:00
Leonardo de Moura
905a1095f9 fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:41:23 -07:00
Leonardo de Moura
62483b793f feat(library/standard): add notation for symm, trans and subst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 22:49:12 -07:00
Leonardo de Moura
ebf34f2fe9 refactor(library/standard): mark 'not' as transparent 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 22:14:15 -07:00
Leonardo de Moura
d84a4bea5f chore(library/standard): port (an older version of) Floris's nat library to Lean 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 20:31:28 -07:00
Leonardo de Moura
48b902dc37 feat(library/unifier): solve constraints of the form '(max l1 l2) =?= 0' and '(imax l1 l2) =?= 0' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 20:30:51 -07:00
Leonardo de Moura
fd0deb4555 feat(library/standard): add basic properties of binary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 17:48:30 -07:00
Leonardo de Moura
a533bf29da fix(library/unifier): broken optimization was missing solution 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 17:41:22 -07:00