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
..
examples	refactor(library): add 'eq' and 'ne' namespaces	2014-09-04 18:41:06 -07:00
cast.lean	feat(frontends/lean): add 'reducible' modifier for controlling which	2014-09-19 15:54:32 -07:00
connectives.lean	feat(frontends/lean): definitions are opaque by default	2014-09-19 15:54:32 -07:00
core.md	refactor(library/logic): move files in classes directory to core	2014-09-16 13:13:01 -07:00
decidable.lean	refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.	2014-09-19 15:54:32 -07:00
eq.lean	feat(library): changes in eq.lean sigma.lean and category.lean	2014-09-26 19:45:23 -04:00
identities.lean	refactor(library/logic): move files in classes directory to core	2014-09-16 13:13:01 -07:00
if.lean	refactor(library/logic): move files in classes directory to core	2014-09-16 13:13:01 -07:00
inhabited.lean	refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.	2014-09-19 15:54:32 -07:00
instances.lean	feat(frontends/lean): definitions are opaque by default	2014-09-19 15:54:32 -07:00
nonempty.lean	refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.	2014-09-19 15:54:32 -07:00
prop.lean	feat(frontends/lean): add 'reducible' modifier for controlling which	2014-09-19 15:54:32 -07:00
quantifiers.lean	feat(frontends/lean): definitions are opaque by default	2014-09-19 15:54:32 -07:00