Commit graph

7189 commits

Author SHA1 Message Date
Floris van Doorn
7a780b1b60 feat(hott): various minor changes in the HoTT library 2015-08-04 13:01:11 +02:00
Leonardo de Moura
0309a1e131 fix(tests/lean/extra/show_goal_bag): adjust test to recent changes in the standard library 2015-08-04 06:52:20 +02:00
Jeremy Avigad
9ff0097223 refactor(library/algebra/{lattice,order},library/data/nat): split lattice from order, make nat an instance of discrete linear order 2015-08-03 22:41:56 -04:00
Jeremy Avigad
0def951efa refactor(library/data/nat/sub,*): get rid of diff, tidy some max and min theorems 2015-08-03 22:41:56 -04:00
François G. Dorais
131b344519 feat(library/algebra/group_power): add times (additive variant of power) 2015-08-04 01:58:57 +02:00
Rob Lewis
e004ed8cba feat(library/algebra): add one directional versions of iff theorems 2015-08-03 17:16:18 -04:00
Rob Lewis
78942a0689 fix(library/data/real): fix num -> rat -> real coercion chain 2015-08-03 16:38:42 -04:00
Rob Lewis
4dd4d7b3b8 style(library/data): clean up proofs in pnat and real 2015-08-03 15:02:03 -04:00
Rob Lewis
82a9bc757a feat(library/algebra): move theorems from real to algebra 2015-08-03 15:01:32 -04:00
Rob Lewis
5c2fe1c3af refactor(real/complete): put limit sequence construction in a section 2015-08-03 11:20:26 -04:00
Rob Lewis
ba2dda08d3 feat(library/data/real): prove infimum property" 2015-08-03 11:16:56 -04:00
Soonho Kong
795728267d doc(emacs/README.md): update MELPA instruction 2015-08-03 09:27:16 -04:00
Leonardo de Moura
60ba3d15ff feat(library/data/matrix): add basic matrix module 2015-08-01 19:33:31 +01:00
Jeremy Avigad
36c7aad6ee fix(library/data/rat/basic): define pow before migrate 2015-08-01 18:23:36 +01:00
François G. Dorais
343b9e62c7 feat(library/data/fin): add foldl and foldr 2015-08-01 18:17:08 +01:00
Leonardo de Moura
1f304ad4b9 fix(frontends/lean/pp): pretty printing 'binder'
This commit also replaces many occurrences of 'binders' with 'binder'.
2015-07-31 11:27:38 -07:00
Leonardo de Moura
3b742c5d69 refactor(library/data/real/complete): use 'em' instead of 'decidable.em'
It is slightly faster since it avoids type class resolution.
It looks more readable too.
Note that em is not axiom anymore. It is a theorem based on choce.
2015-07-31 10:57:53 -07:00
Leonardo de Moura
381c3d5e35 feat(library/data/vec): transfer more theorems from list to vec 2015-07-31 09:59:58 -07:00
Leonardo de Moura
8f5a760b89 feat(frontends/lean/elaborator): display the whole proof state in option "--goal"
see issue #755
2015-07-31 08:56:17 -07:00
Leonardo de Moura
a53ac25ca8 chore(library): remove outdated comments 2015-07-31 08:37:24 -07:00
Rob Lewis
01af780b6e feat(library/data/real): clean up proof of supremum property 2015-07-31 08:28:37 -07:00
Rob Lewis
1693932c9f feat(library/algebra/group): add theorem to comm group 2015-07-31 08:28:37 -07:00
Rob Lewis
0c65468db3 feat(library/data/real): remove remaining sorrys from proof of supremum property 2015-07-31 08:28:36 -07:00
Rob Lewis
25aa5b3939 feat(library/data/nat): define least function for nat 2015-07-31 08:28:36 -07:00
Rob Lewis
7d6b595289 feat(library/data/real): complete proof of the supremum property pending two integer theorems 2015-07-31 08:28:36 -07:00
Rob Lewis
954e30b59a feat(library/data/real): add more theorems to reals 2015-07-31 08:28:36 -07:00
Rob Lewis
f929f82cb4 feat(library/data/real): fill in remaining sorrys in supremum property proof 2015-07-31 08:28:36 -07:00
Rob Lewis
f88038c3e7 feat(library/algebra/field): add missing theorems to field 2015-07-31 08:28:36 -07:00
Rob Lewis
b4b08aca32 feat(library/data/real): more progress toward supremum property 2015-07-31 08:28:26 -07:00
Rob Lewis
2fdf1e599e feat(library/algebra/ordered_group): add missing theorems to ordered group 2015-07-31 09:10:57 -04:00
Rob Lewis
ebbad9e70d chore(library/data/real): fill in sorrys in supremum property proof 2015-07-31 09:10:57 -04:00
Rob Lewis
c9daf7cbb9 feat(library/algebra/ordered_field): add missing theorems to ordered field 2015-07-31 09:10:57 -04:00
Rob Lewis
7a4947cfe1 feat(library/algebra/real): significant progress toward supremum property 2015-07-31 09:10:57 -04:00
Rob Lewis
601f824baf feat(library/data/real): compare a real and a sequence pointwise to compare two reals 2015-07-31 09:10:57 -04:00
Rob Lewis
d63010b7df feat(library/data/real): prove more about embedding Q into R 2015-07-31 09:10:57 -04:00
Rob Lewis
a670f21e78 feat(library/data/real): begin proving supremum property 2015-07-31 09:10:57 -04:00
Rob Lewis
3a97079920 feat(library/data/real): finish coercions from rat to real 2015-07-31 09:10:56 -04:00
Leonardo de Moura
811bae5566 feat(library/data/vec): expand vec 2015-07-30 23:17:01 -07:00
Leonardo de Moura
8dc2246a83 refactor(library/theories/group_theory/action): improve compilation time 2015-07-30 20:58:38 -07:00
Leonardo de Moura
44518fcab1 refactor(library/theories/group_theory): move diff to nat 2015-07-30 20:14:48 -07:00
Leonardo de Moura
0a29581b0e feat(library/data/vec): add more theorems to vec (vectors as subtypes) 2015-07-30 18:09:10 -07:00
Leonardo de Moura
f264adfa92 fix(library/export): bug in --export-all option 2015-07-30 17:23:38 -07:00
Leonardo de Moura
9bf64c10fd feat(library/export): export the whole environment when using "--expor-all" 2015-07-30 15:04:49 -07:00
Soonho Kong
bed751a2d7 feat(emacs/lean-settings.el): add lean-keybinding customize group
close #758
2015-07-30 11:33:17 -07:00
Leonardo de Moura
656b642c4a fix(frontends/lean): identifier size when using unicode
see issue #756
2015-07-30 11:32:24 -07:00
Leonardo de Moura
a39cac4fad feat(frontends/lean): improve '--info' command line option
see issue #756
2015-07-30 11:05:39 -07:00
Soonho Kong
c390550340 feat(emacs/lean-mode.el): add show-goal-at-pos and show-id-keyword-info in the menu 2015-07-30 10:46:47 -07:00
Soonho Kong
46a79ec43d feat(emacs/lean-mode.el): add lean-show-id-keyword-info
close #756
2015-07-30 10:46:10 -07:00
Théo Zimmermann
698b368f01 fix(doc): fix confusion between Prop and Bool
this fix assumes that Prop and Bool are two different things but even if they were the same thing, using the two names would only confuse the reader
2015-07-30 10:21:43 -07:00
Théo Zimmermann
923d12553e fix(doc): correct two more mistakes
- fix a mistake in code example
- fix singular/plural confusion
2015-07-30 10:21:42 -07:00