Floris van Doorn
|
c884e7bbb9
|
feat(hott/algebra): define additive structures to be multiplicative structures
|
2016-09-19 22:13:35 -04:00 |
|
Leonardo de Moura
|
cc8d9bc7ff
|
refactor(hott): replace 'assert'-expr with 'have'-expr
|
2016-02-29 12:11:17 -08:00 |
|
Leonardo de Moura
|
768ba1c363
|
refactor(library/hott): remove more unnecessary annotations
|
2016-02-25 14:30:00 -08:00 |
|
Floris van Doorn
|
2325d23f68
|
feat(hott): port nat and int from the standard library
|
2015-12-09 12:36:11 -08:00 |
|
Floris van Doorn
|
46739c8b70
|
feat(hott/algebra): port abstract structures
|
2015-12-09 12:34:06 -08:00 |
|