Jeremy Avigad
0d982cceed
feat(library/algebra/ring): begin theory of semirings and rings
2014-11-14 17:27:35 -08:00
Jeremy Avigad
1ed7794264
feat(library/algebra/group): add theorems for calculation
2014-11-13 20:44:58 -08:00
Floris van Doorn
bf27a17dec
style(library): add some comments
2014-11-08 19:12:54 -08:00
Floris van Doorn
8c7fdd3708
style(library): rename set_category to discrete_category
2014-11-08 19:12:54 -08:00
Floris van Doorn
930cc11684
doc(algebra): update markdown files
2014-11-08 19:12:54 -08:00
Floris van Doorn
cd33d2e96d
refactor(typeof): move typeof to general_notation
2014-11-08 19:12:54 -08:00
Jeremy Avigad
4a955c0f92
feat(library/algebra/order): begin theory of orders
...
feat(library/algebra/order): begin theory of orders
2014-11-08 19:07:59 -08:00
Jeremy Avigad
c28227d7a1
feat(library/algebra/group): add multiplicative and additive structures
2014-11-07 10:23:37 -08:00
Leonardo de Moura
b177c84b06
feat(library/logic): add well-founded recursion
...
It also removes the old well-founded induction theorem based on
classical principles
2014-11-06 14:49:53 -08:00
Floris van Doorn
d8a616fa70
refactor(library): major changes in the library
...
I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.
Changes:
- in multiple files make more use of variables
- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).
- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
require piext)
- in theorems where casts are used in the statement use eq.rec_on
instead of eq.drec_on
- in category split basic into basic, functor and natural_transformation
- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major). You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.
- lots of minor changes
2014-11-03 18:45:12 -08:00
Leonardo de Moura
4bdee07af2
refactor(library/algebra/category/basic): use calc assistant
2014-10-31 09:49:45 -07:00
Leonardo de Moura
e24225fabf
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
2014-10-21 15:39:47 -07:00
Leonardo de Moura
6c7e23ecaa
refactor(library): use 'reserve' notation in the standard library
2014-10-21 15:39:47 -07:00
Leonardo de Moura
40fb66bf07
feat(frontends/lean): change default precedence to 1
2014-10-20 18:40:55 -07:00
Leonardo de Moura
4a9e725ca7
refactor(library/algebra/category/morphism): make sure bug #231 has been fixed
2014-10-13 20:56:40 -07:00
Leonardo de Moura
9edf780a00
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem
2014-10-13 18:35:11 -07:00
Leonardo de Moura
a26618e0f2
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
2014-10-12 13:06:00 -07:00
Leonardo de Moura
f832212fc8
refactor(library/algebra/category): remove unnecessary sections
2014-10-11 16:40:26 -07:00
Floris van Doorn
c630b5ddb2
feat(library/algebra/category): use variables instead of parameters
2014-10-11 16:40:18 -07:00
Leonardo de Moura
d6d0593afb
refactor(library): remove some unnecessary sections
2014-10-10 16:33:58 -07:00
Leonardo de Moura
052bc6ff20
fix(frontends/lean/elaborator): better specific universe detection
2014-10-09 14:43:07 -07:00
Leonardo de Moura
8f1b6178a7
chore(*): minimize the use of parameters
2014-10-09 07:13:06 -07:00
Leonardo de Moura
f9e8503005
chore(library/algebra/category): add workaround
2014-10-09 00:05:37 -07:00
Leonardo de Moura
8c5d3392c7
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
2014-10-08 23:44:09 -07:00
Floris van Doorn
0a58e3d1ae
feat(algebra/category/): minor additions, start on adjunction
2014-10-08 23:14:44 -07:00
Floris van Doorn
57bee2a659
feat(binary.lean): add helper theorem for associative functions
2014-10-08 23:14:44 -07:00
Floris van Doorn
8d376b93cd
feat(category): split category.lean in different files; add more constructions and theorems about isos
2014-10-08 23:14:44 -07:00
Leonardo de Moura
744cee8dd8
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228
2014-10-07 18:02:15 -07:00
Leonardo de Moura
73aa024c31
refactor(library/logic): remove 'core' subdirectory
2014-10-05 10:50:13 -07:00
Leonardo de Moura
716cd4d651
refactor(library): rename namespace eq_ops to eq.ops
2014-10-01 17:51:17 -07:00
Leonardo de Moura
21be308884
feat(frontends/lean/inductive_cmd): infer implicit argument annotation after elaboration, allow user to disable it by using '()' annotation, closes #210
2014-09-29 11:11:17 -07:00
Leonardo de Moura
9c55bbb871
feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208
2014-09-29 08:18:10 -07:00
Floris van Doorn
3a95734fae
feat(library): changes in eq.lean sigma.lean and category.lean
...
in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5
in sigma.lean, finish proving equality of triples
in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator
2014-09-26 19:45:23 -04:00
Floris van Doorn
5396e422d2
feat(library): add constructions of categories, some changes in eq, sigma and path
...
in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach
2014-09-26 19:45:23 -04:00
Leonardo de Moura
08ccd58eb6
feat(frontends/lean): add 'reducible' modifier for controlling which
...
definitions are unfolded during elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8
feat(frontends/lean): definitions are opaque by default
2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef
feat(frontends/lean): allow transient classes/instances, i.e.,
...
classes/instances that are not saved in .olean files
2014-09-19 15:54:32 -07:00
Leonardo de Moura
4b51d50ad4
fix(frontends/lean/elaborator): coercion overloading
2014-09-16 15:12:20 -07:00
Jeremy Avigad
74cb289d48
refactor(library): rename algebra directory to struc, move categories.lean to algebra
2014-09-16 13:13:01 -07:00
