Commit graph

7173 commits

Author SHA1 Message Date
Leonardo de Moura
b31ab7d77a feat(compiler,frontends/lean): add #compile command for debugging purposes, add compiler module 2015-09-11 10:49:07 -07:00
Leonardo de Moura
8666c92bae feat(library,library/definitional): tag auxiliary recursors automatically generated by Lean 2015-09-11 10:08:54 -07:00
Rob Lewis
8d1f449491 refactor(library/data/real): move and rename theorems 2015-09-11 08:52:53 -07:00
Rob Lewis
8e428f2d3f fix(src/library/definitional/equations.cpp): fix typo in error message 2015-09-11 08:52:53 -07:00
Leonardo de Moura
84a80b343a chore(runtime/cpp): fix style 2015-09-11 08:44:18 -07:00
Leonardo de Moura
e36fde4d45 feat(runtime/cpp): add runtime library for Lean -> C++ compiler 2015-09-11 08:44:18 -07:00
Soonho Kong
f941af03ba feat(CMakeLists.txt): install *.md in standard/hott libraries
close #823
2015-09-10 18:13:47 -04:00
Leonardo de Moura
88739f0199 fix(tests/shared/env): memory leaks in test program 2015-09-09 10:02:18 -07:00
Leonardo de Moura
f452cabc34 feat(api/exception): add lean_exception_get_detailed_message 2015-09-08 18:00:23 -07:00
Leonardo de Moura
eec3780c6d feat(api): add API (lean_exception_to_pp_string) for pretty printing exceptions 2015-09-08 17:46:07 -07:00
Leonardo de Moura
7289e386cb feat(api/lean_expr): add lean_macro_def_eq and lean_macro_def_to_string 2015-09-08 16:51:32 -07:00
Leonardo de Moura
36d2c63ad0 feat(api): add APIs for parsing files, commands and expressions 2015-09-08 16:44:33 -07:00
Leonardo de Moura
3c1d6ec67a feat(library/algebra/algebra): add link to complete lattices module 2015-09-04 13:04:36 -07:00
Sebastian Reuße
f8a773be11 chore(library/algebra): remove obsolete link. 2015-09-04 09:41:34 +02:00
Leonardo de Moura
1fdbd681cc feat(frontends/lean/builtin_exprs): name hypothesis in suffices
closes #817
2015-09-03 16:09:39 -07:00
Rob Lewis
e722120e34 fix(library/data/rat/order): declare decidable_le an instance 2015-09-03 15:43:07 -07:00
Jeremy Avigad
7c966e3d02 fix(src/emacs/lean-syntax.el): highlight identifiers after 'proposition' and 'corollary' 2015-09-03 15:38:27 -07:00
Jeremy Avigad
2ab7928257 refactor(library/data/set/basic): standardize intro and elim theorem names 2015-09-03 15:38:27 -07:00
Leonardo de Moura
57115688ea chore(util/thread): fix style 2015-09-03 15:07:55 -07:00
Leonardo de Moura
ade3f80089 fix(util/thread,init/init): initialization problem 2015-09-03 14:43:50 -07:00
Leonardo de Moura
3c50a9cff8 fix(util/thread): LEAN_AUTO_THREAD_FINALIZATION on OSX 2015-09-03 14:18:31 -07:00
Leonardo de Moura
1dc1574ad4 fix(frontends/lean/parse_table): do not add 'no_info' annotation in tactic expressions 2015-09-02 20:51:06 -07:00
Leonardo de Moura
634c0b5e9d feat(library/tactic,frontends/lean): propagate new options back to elaborator 2015-09-02 20:34:14 -07:00
Leonardo de Moura
6f88e06472 fix(tests/shared/CMakeLists): typos in test scripts 2015-09-02 12:49:43 -07:00
Leonardo de Moura
524e507022 fix(util/thread): make sure threads are finalized when using the Lean C API and threads are created by the host system 2015-09-02 12:23:10 -07:00
Leonardo de Moura
cae2271818 refactor(hott/algebra/category/adjoint): rewrite expensive proof
see #815
2015-09-01 16:59:14 -07:00
Floris van Doorn
a8964adb9c fix(hott): make sure there are no sorry's visible 2015-09-01 15:17:46 -07:00
Floris van Doorn
7e52c49dce feat(hott): many changes is the HoTT library
Prove that 'is_left_adjoint F' is a mere proposition, although this proof is commented out because it takes ~10 seconds
2015-09-01 15:17:46 -07:00
Floris van Doorn
f555120428 feat(types/eq): add general encode-decode method 2015-09-01 15:17:46 -07:00
Floris van Doorn
f4892db432 feat(types.trunc): prove the principle of unique choice 2015-09-01 15:17:46 -07:00
Floris van Doorn
c24fd508b6 feat(hott/types): add more about pathovers in type constructors, prove that double negation elimination doesn't hold universally 2015-09-01 15:17:46 -07:00
Floris van Doorn
cfddfdfa84 feat(hott/types): add characterization of lift, prove that Type.{u} is not an hset 2015-09-01 15:17:46 -07:00
Floris van Doorn
9a439d4a4e feat(library.md): update reference to classical axiom 2015-09-01 15:17:46 -07:00
Simon Cruanes
8ce3d44302 doc(vim/README): add a readme for vim syntax coloring 2015-09-01 15:08:16 -07:00
Simon Cruanes
0a307bf76c fix(vim): small fixes 2015-09-01 15:08:07 -07:00
Simon Cruanes
94b68a8263 fix(vim/syntax/lean): match notations in vim syntax 2015-09-01 15:07:54 -07:00
Simon Cruanes
3188a42259 feat(vim): add basic syntax support for vim 2015-09-01 15:07:43 -07:00
Leonardo de Moura
44c6e92a64 fix(tests/lean): notation ℕ is now defined in the top-level 2015-09-01 14:58:14 -07:00
Jeremy Avigad
072971f3bb feat(library/data/finset/comb,library/data/set/basic): define set complement 2015-09-01 14:47:19 -07:00
Jeremy Avigad
840ef98829 refactor(library/init/nat): make \nat notation available at top level 2015-09-01 14:47:19 -07:00
Jeremy Avigad
51e0d31304 refactor(library/algebra/ordered_ring,ordered_field): move theorems from ordered_field to ordered_ring 2015-09-01 14:47:19 -07:00
Jeremy Avigad
7d72c9b6b5 refactor(library/algebra/{field,ordered_field}, library/*): more renaming, setting implicit arguments
Many theorems for division rings and fields have stronger versions for discrete fields, where we
assume x / 0 = 0. Before, we used primes to distinguish the versions, but that has the downside
that e.g. for rat and real, all the theorems are equally present. Now, I qualified the weaker ones
with division_ring.foo or field.foo. Maybe that is not ideal, but let's try it.

I also set implicit arguments with the following convention: an argument to a theorem should be
explicit unless it can be inferred from the other arguments and hypotheses.
2015-09-01 14:47:19 -07:00
Jeremy Avigad
93c2d1e9d0 refactor(library/algebra/ordered_field): rename theorems to maintain consistency with other parts of the library 2015-09-01 14:47:19 -07:00
Jeremy Avigad
92af727daf fix(library/data/real/{basic,division,order}: use notation for 0 and 1
These changes were needed because e.g. real.add_zero was "x + zero = x", and rewrite
would not match it to a goal "t + 0".

The fix was a lot harder than I expected. At first, migrate failed with resource
errors. In the end, what worked was this: I defined the coercion from num to real
directly (rather than infer num -> nat -> int -> rat -> real).

I still don't understand what the issues are, though. There are subtle issues with
numerals and coercions and migrate.

(We are not alone. Isabelle also suffers from the fact that there are too many
"zero"s and "one"s.)
2015-09-01 14:47:19 -07:00
Joe Hendrix
79b77b1011 fix(api): lean_ios_is_std returned incorrect result 2015-09-01 14:40:39 -07:00
Joe Hendrix
91dc9c7bd9 fix(api): fix typos in function name and comment 2015-09-01 14:40:34 -07:00
Leonardo de Moura
c84e886c7b fix(frontends/lean/notation_cmd): fixes #808
This commit and 2b1d2c fixes #808
2015-08-31 18:05:58 -10:00
Leonardo de Moura
08169c5ac2 fix(library/unifier): fixes #809
Daniel is correct when he says the interaction between choice
case-splits, delta case-splits, and coercions can be subtle.

I believe the following condition
https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111
reduces counter-intuitive behavior. Example, the coercion should not
influence the resulting type.
BTW, by removing this condition, many files in the library broke when I
tried to compile from scratch

      make clean-olean
      make

I used the following workaround. Given a delta-delta constraint

           f a =?= f b

If the terms are types, and no case-split will be performed, then
the delta-delta constraint is eagerly solved.
In principle, we don't need the condition that the terms are types.
However, many files break if we remove it. The problem is that many files in the standard
library are abusing the higher-order unification procedure. The
elaboration problems are quite tricky to solve.
I use the extra condition "the terms are types" because usually if they
are, "f" is morally injective, and we don't really want to unfold it.

Note that the following two cases do not work

     check '{1, 2, 3}
     check insert 1 (insert 2 (insert 3 empty))

Well, they work if we the num namespace is open, and they are
interpreted as having type (finset num)
2015-08-31 17:59:30 -10:00
Leonardo de Moura
3b19de1974 feat(library/data/num): show that num has decidable equality 2015-08-31 17:47:07 -10:00
Leonardo de Moura
63b93cf762 refactor(library/data/set/finite): make proof more robust 2015-08-31 17:26:24 -10:00