Jeremy Avigad
|
d48a332876
|
refactor(library/data/prod): move specialized theorems to quotient
|
2015-02-01 11:17:45 -08:00 |
|
Floris van Doorn
|
7bfbe039d9
|
refactor(data.prod): move theorems about products from data.quotient.util to data.prod.thms
|
2014-11-22 17:44:12 -08:00 |
|
Leonardo de Moura
|
60eac0195d
|
feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures
|
2014-11-04 09:10:25 -08:00 |
|
Leonardo de Moura
|
86591c7272
|
refactor(library/data/prod): cleanup
|
2014-10-05 13:38:08 -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
|
baf4c01de8
|
feat(frontends/lean): definitions are opaque by default
|
2014-09-19 15:54:32 -07:00 |
|
Leonardo de Moura
|
e3e2370a38
|
feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-16 18:03:40 -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 |
|
Leonardo de Moura
|
8c11dc1ecd
|
chore(library/data/quotient): rename aux.lean to util.lean (fix problem with cloning lean repository on Windows machine)
See
http://stackoverflow.com/questions/3689137/error-git-checkout-index-unable-to-create-file
for additional details
|
2014-09-11 14:57:15 -07:00 |
|