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

5846 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
ced742083a feat(library/init/quot): add helper function quot.rec_on_subsingleton₂ 2015-04-01 13:04:41 -07:00
Leonardo de Moura
ed1acd9fb0 feat(library/init): move propext to init/quot, add Jeremy's funext theorem 2015-04-01 12:36:33 -07:00
Leonardo de Moura
0da4f191fc feat(library/init/quot): add rec_on for subsingleton types 2015-04-01 11:57:39 -07:00
Leonardo de Moura
ce5e83eb3e refactor(library/init): move subsingleton to init folder 2015-04-01 11:57:29 -07:00
Leonardo de Moura
b960e123b1 feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
Leonardo de Moura
82833bcbe8 fix(tests/lean/struct_class): add setoid to expected output 2015-03-31 22:03:57 -07:00
Leonardo de Moura
a52cb009dc refactor(library): reorganize init folder and add setoid 2015-03-31 19:56:05 -07:00
Leonardo de Moura
6e6cc749a8 feat(library/logic/axioms): break prop_complete into propext and em 
The user may want to use propext without assuming em.
 2015-03-31 18:51:43 -07:00
Leonardo de Moura
e35de54cee feat(library/data/list/basic): add aux theorems 2015-03-31 18:38:05 -07:00
Leonardo de Moura
4eb270a572 fix(frontends/lean/pp): extra space 2015-03-31 15:07:32 -07:00
Leonardo de Moura
26c914173c feat(frontends/lean): add --profile option 2015-03-31 11:53:55 -07:00
Leonardo de Moura
4c0ce9a619 feat(library/data/list/basic): missing theorems 2015-03-30 19:11:45 -07:00
Leonardo de Moura
46777fdd1d fix(frontends/lean/migrate_cmd): bug when using migrate command with option --to_axiom 2015-03-30 16:22:06 -07:00
Soonho Kong
3132d229c0 chore(travis): change notifications, turn off cov build 2015-03-30 18:32:48 -04:00
Leonardo de Moura
8c76419c60 fix(frontends/lean/decl_cmds): error localization problem for recursive equations 2015-03-30 13:30:29 -07:00
Leonardo de Moura
87f6fc6b6a feat(library/algebra/ring): remove sorrys 2015-03-30 11:55:48 -07:00
Leonardo de Moura
56af7ba535 feat(library/algebra/ordered_ring): remove sorry 2015-03-30 11:01:26 -07:00
Leonardo de Moura
3d4a02089a feat(library/logic/examples/propositional): add different encoding 2015-03-30 07:13:19 -07:00
Leonardo de Moura
9d34431bb6 feat(library/logic/examples/propositional/soundness): cleanup precedence levels 2015-03-30 05:42:47 -07:00
Leonardo de Moura
5ef88bfbc8 feat(library/logic/examples/propositional): add example based on Floris Coq files formalizing propositional Calculus 2015-03-30 05:12:29 -07:00
Leonardo de Moura
299cbe4b25 feat(library/data/bool): add auxiliary theorems for bool 2015-03-30 04:55:28 -07:00
Leonardo de Moura
42fe87d7cc feat(library/data/list/basic): add sublist predicate 2015-03-30 03:20:42 -07:00
Leonardo de Moura
66bb22f268 feat(library/data/list/basic): cleanup 2015-03-30 02:14:33 -07:00
Leonardo de Moura
ec1a60b02c feat(library/init/logic): add helper function for proving decidable equality 2015-03-30 02:14:26 -07:00
Leonardo de Moura
cb2a5eeb3c feat(frontends/lean/inductive_cmd): local notation in inductive decls 2015-03-30 02:14:26 -07:00
Leonardo de Moura
033f3b630d feat(frontends/lean/scanner): allow upper-case greek letters in identifiers but Pi and Sigma 2015-03-30 02:14:26 -07:00
Soonho Kong
47c0ae5914 fix(bin/linja): download ninja to a temporary directory 
Assume that we have two linja processes running on a system where there
is no ninja installed. Then, the first linja process downloads ninja
from github. If the internet is slow, the second linja process can pick
up the incomplete ninja binary and execute it, which causes an
exception (i.e. "Malformed Mach-o file" error on OSX). An example build
trace is at

    https://s3.amazonaws.com/archive.travis-ci.org/jobs/56366771/log.txt

This commit fixes the problem by downloading ninja to a temporary
directory and copy it to "lean/bin/ninja" when it's completed.
 2015-03-30 01:20:24 -04:00
Soonho Kong
3ac29fae43 fix(util/lua.cpp): 'implicit conversion of nullptr constant to bool' warning 
clang-3.6.0 generated the following warning:

/Users/soonhok/work/lean/src/util/lua.cpp:49:12: warning: implicit conversion of nullptr constant to 'bool' [-Wnull-conversion]
    return nullptr;
    ~~~~~~ ^~~~~~~
           false
 2015-03-29 23:06:22 -04:00
Soonho Kong
8243ed6339 fix(test*.sh): allow spaces in filename 
fix #515
 2015-03-28 23:29:52 -04:00
Soonho Kong
0d1da89cf1 chore(.gitignore): update 2015-03-28 23:29:41 -04:00
Soonho Kong
93a3ef1447 fix(bin/linja): escape ' ' in depfiles differently 
' ' ==> '\\ ' in .d files

fix #515
 2015-03-28 22:38:13 -04:00
Soonho Kong
f72f4cf441 fix(bin/linja): add '$' and ' ' cases to escape_ninja_char 
This is related to #513
 2015-03-28 22:38:13 -04:00
Soonho Kong
9fb44c1e93 chore(.gitignore): add compile_commands.json 2015-03-28 22:38:13 -04:00
Soonho Kong
7c5339d64e fix(CMakeLists.txt): quote CMake variables 
close #513
 2015-03-28 22:38:11 -04:00
Leonardo de Moura
cbac8d1300 chore(README): avoid duplication 2015-03-28 16:23:32 -07:00
Leonardo de Moura
5b9d52c0dd refactor(library/data/int/order): cleanup 2015-03-28 12:58:40 -07:00
Leonardo de Moura
ea3407d06d fix(library/tactic): valgrind warnings for still reachable memory 2015-03-28 12:32:57 -07:00
Leonardo de Moura
88495f9d59 fix(*): remove unnecessary null pointer checks 
closes #514
 2015-03-28 12:16:39 -07:00
Soonho Kong
0cda3f7cbf fix(bin/linja): only strip flycheck message in linja 
Removing empty lines for FlyCheck messages was added by
4266b8c7a3. We had somecases where
Flycheck messages start with an empty line instead of `FLYCHECK_BEGIN
ERROR` in Windows7 + Python2 env. I think it's because of the different
newline character problem (LF, LFCR). My solution was to remove all
empty lines, which was too much. Now, I think striping should be enoguh.

fix #512
 2015-03-28 07:56:32 -04:00
Leonardo de Moura
1b15036dba feat(library/definitional): automatically add attribute [unfold-c] to cases_on, brec_on and rec_on 
see #496
 2015-03-27 19:12:17 -07:00
Leonardo de Moura
75621df52b feat(frontends/lean): uniform notation for lists in tactics 
closes #504
 2015-03-27 17:54:48 -07:00
Leonardo de Moura
242f8ba048 feat(frontends/lean/elaborator): include number of unsolved goals 
See #509
 2015-03-27 14:54:41 -07:00
Rob Lewis
abcc56a2a7 feat(library/algebra):refactor field and ordered_field more appropriately 2015-03-27 11:54:11 -07:00
Rob Lewis
b79f600fbc style(library/algebra/ordered_field):fix indentation, shorten calc statements 2015-03-27 11:52:30 -07:00
Rob Lewis
94b9aaea45 feat(library/algebra/ordered_field): prove more theorems 2015-03-27 11:52:30 -07:00
Rob Lewis
a1028922bd feat(library/algebra/ordered_field): complete proofs of many theorems. Define discrete linear ordered field 2015-03-27 11:52:30 -07:00
Rob Lewis
4099de7754 feat(library/algebra/field): redefine field so that 1/0=0. Many theorems lose hypotheses in discrete setting. 2015-03-27 11:52:29 -07:00
Rob Lewis
365f1ebcb6 feat(library/algebra/ordered_field): prove more theorems for ordered field 2015-03-27 11:45:57 -07:00
Rob Lewis
11f82eacfb feat(library/algebra/ordered_field.lean): add ordered fields 2015-03-27 11:45:57 -07:00
Leonardo de Moura
223ef58db9 fix(kernel/equiv_manager): typo 2015-03-27 10:44:09 -07:00