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

94 commits

Author SHA1 Message Date
Rob Lewis
87ec5ada07 fix(analysis/metric_space): unnecessary import, style, remove unnecessary lines 2016-02-04 11:03:28 -08:00
Rob Lewis
a675a5ede2 fix(algebra/ordered_field, analysis/real_limit): generalize theorem to ordered fields 2016-02-04 11:03:28 -08:00
Rob Lewis
f402f322aa feat(theories/analysis): add theorems about convergent sequences, functions, and continuity 2016-02-04 11:03:28 -08:00
Rob Lewis
40a1371cd0 feat(theories/analysis): define real square roots 2016-02-04 11:03:28 -08:00
Rob Lewis
796e16bdb7 feat(library/theories/analysis): add theorems about convergent functions in metric spaces 2016-02-04 11:03:28 -08:00
Leonardo de Moura
cb12b9b876 refactor(library): cleanup proofs 
Fixed proofs that broke when we tried to implement a "checkpoint" have.
 2016-02-03 19:52:23 -08:00
Jeremy Avigad
86fc326e08 refactor/feat(library/theories/analysis/*): reorganize analysis library and add some theorems 2016-01-16 10:53:56 -08:00
Jeremy Avigad
d9118ded76 feat(library/theories/topology/basic): show that generated topology is initial 2016-01-03 18:52:25 -08:00
Jeremy Avigad
4289daddcb refactor(library/data/{set,finset}/basic,library/*): change notation for image to tick mark 2016-01-03 18:52:25 -08:00
Jeremy Avigad
31aa256b99 feat(library/theories/measure_theory/sigma_algebra): start with definition and properties of sigma algebras 2016-01-03 18:52:25 -08:00
Jeremy Avigad
12a69bad04 refactor(library/data/finset/basic,library/*): get rid of finset singleton 2015-12-31 15:16:57 -08:00
Jeremy Avigad
86b64cf43b feat(library/data/set/*,library/algebra/group_bigops): better finiteness lemmas, reindexing for big operations 2015-12-31 15:16:57 -08:00
Leonardo de Moura
f177082c3b refactor(*): normalize metaclass names 
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
 2015-12-28 10:39:15 -08:00
Jeremy Avigad
395eab7c2c feat(library/theories/topology/basic): start on topology (with Jacob Gross) 2015-12-26 10:29:58 -08:00
Jeremy Avigad
d83e5d25fc feat(library/theories/measure_theory/extended_real): start on extended reals 2015-12-24 16:27:48 -05:00
Jeremy Avigad
84cdf3d36d feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis 2015-12-22 16:39:13 -05:00
Jeremy Avigad
08fbf127c6 feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance 2015-12-22 16:39:13 -05:00
Jeremy Avigad
6913eb0c76 refactor(library/init/subtype.lean): put subtype notation in the namespace 
The notation { x : A | P x } is overloaded in set, and is ambiguous.
 2015-12-22 16:39:13 -05:00
Jeremy Avigad
0e3b13f1a0 refactor(library/algebra): combine group_bigops and group_set_bigops 2015-12-22 16:39:13 -05:00
Sebastian Ullrich
2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic 
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
 2015-12-14 10:14:02 -08:00
Leonardo de Moura
49eae56db4 test(library/theories/group_theory): test auto-include in the group theory library 2015-12-13 13:40:54 -08:00
Leonardo de Moura
b94e31a72c refactor(library): remove algebra namespace 2015-12-05 23:50:01 -08:00
Leonardo de Moura
9bedbbb739 refactor(library,hott): remove coercions between algebraic structures 
They are classes, and mixing coercion with type class resolution is a
recipe for disaster (aka counterintuitive behavior).
 2015-11-11 11:57:44 -08:00
Jeremy Avigad
697df0e68c refactor(library/*): use type classes for div and mod 2015-11-08 14:04:59 -08:00
Jeremy Avigad
2beb0030d6 refactor(library/*): protect sub in nat, div in nat and int 2015-11-08 14:04:59 -08:00
Jeremy Avigad
9e5a27dc77 refactor(library/{pnat,rat,real}/*): protect theorems in pnat and rat 2015-11-08 14:04:59 -08:00
Jeremy Avigad
da5bd03656 refactor(library/init/nat,library/data/nat/*): chagne dots to underscores in protected names 2015-11-08 14:04:59 -08:00
Jeremy Avigad
6dfaf1863c refactor(library/data/int/{basic,order}): protect theorem names 2015-11-08 14:04:59 -08:00
Jeremy Avigad
7bb2ffb79a refactor(library/data/nat/*): protect some theorems in nat 2015-11-08 14:04:59 -08:00
Leonardo de Moura
33006919b3 refactor(library/theories/group_theory/hom): cleanup definition 2015-11-08 14:04:58 -08:00
Leonardo de Moura
08c061e1fa refactor(library/data/set): remove [reducible] annotation from set operations 2015-11-08 14:04:56 -08:00
Leonardo de Moura
6df31d3406 refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading 2015-11-08 14:04:56 -08:00
Rob Lewis
0aaa8a9770 feat(theories/analysis/real_limit): fix analysis.real_limit 2015-11-08 14:04:56 -08:00
Leonardo de Moura
840f0ea05d fix(library/theories/analysis/real_limit): minor 2015-11-08 14:04:55 -08:00
Leonardo de Moura
9fb59a05f5 fix(library/theories/analysis/metric_space): minor correction 2015-11-08 14:04:55 -08:00
Leonardo de Moura
fbe80d48dc chore(library): remove "set_option pp.*" commands 2015-11-08 14:04:55 -08:00
Leonardo de Moura
ce21996635 feat(library): define custom recursors for nat, and minimize the use of krewrite 2015-11-08 14:04:55 -08:00
Jeremy Avigad
7f88e9ad33 fix(library/data/real,library/theories/group_theory): group theory and real/basic 2015-11-08 14:04:55 -08:00
Jeremy Avigad
ffbb2be6ac fix(library/theories/group_theory): group_theory 2015-11-08 14:04:55 -08:00
Leonardo de Moura
724aacb2c1 fix(library): remove "-[notations]" hack at "open -[notations] algebra" 2015-11-08 14:04:55 -08:00
Leonardo de Moura
26eb6fa849 feat(*): new numeral encoding 2015-11-08 14:04:55 -08:00
Leonardo de Moura
f6d22c0002 fix(library/theories/group_theory/finsubg): fix compilation errors 2015-11-08 14:04:55 -08:00
Leonardo de Moura
07b33ec75e fix(library/data/int,library/data/rat): int and rat 2015-11-08 14:04:54 -08:00
Leonardo de Moura
27b4eb2058 fix(library/data): hf, int, nat, pnat 2015-11-08 14:04:54 -08:00
Leonardo de Moura
3369152559 fix(library/data,library/theories): fin, bag, finset, hf, list, ... 2015-11-08 14:04:54 -08:00
Leonardo de Moura
e6d7e89419 fix(library/data/int,library/data/nat): nat and int 2015-11-08 14:04:54 -08:00
Jeremy Avigad
42c9bdc463 feat(library/theories/analysis/{metric_space,real_limit}: add convergence theorems 2015-09-20 20:51:28 -04:00
Rob Lewis
d6be32e4ef feat(library/theories/analysis): refactor IVT proof, add more general version of IVT 2015-09-17 16:22:46 -04:00
Rob Lewis
856a09d70e chore(library/theories/analysis): make proof of IVT compile faster 2015-09-16 16:44:28 -04:00
Rob Lewis
631b9b3312 feat(library/theories/analysis): clean and simplify proof of IVT 2015-09-16 08:28:11 -07:00