Floris van Doorn
|
c8eee66c5b
|
feat(hott/relation): add equivalence closure of a relation
|
2015-06-25 22:31:41 -04:00 |
|
Floris van Doorn
|
ea0f57aef5
|
feat(hott): various clean-up and small additions
|
2015-06-25 22:31:40 -04:00 |
|
Floris van Doorn
|
ff41886a32
|
feat(nat/bquant): give instances for quantification bounded with le
also add theorems c_iff_c to logic/connectives, where c is a connective
|
2015-06-04 20:14:13 -04:00 |
|
Floris van Doorn
|
2144036cdb
|
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
Also many minor fixes at various places
|
2015-05-18 15:59:55 -07:00 |
|
Jeremy Avigad
|
95dae11670
|
feat(src/emacs/lean-input.el): add abbreviations 'mem', 'subeq', etc.
|
2015-05-11 09:03:56 -07:00 |
|
Jeremy Avigad
|
9beb70b292
|
feat(src/emacs/lean-input.el): add 'empty' as abbreviation for emptyset
|
2015-05-08 20:04:55 +10:00 |
|
Floris van Doorn
|
d4a929febb
|
feat(lean-input): add some notation
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
ee4cba4e0b
|
style(hott): a bit of cleanup
|
2015-04-22 13:06:11 -07:00 |
|
Soonho Kong
|
1f20fb6e9e
|
feat(emacs/lean-input): add not(¬) and iff(↔)
close leanprover/tutorial#81
|
2015-04-02 22:13:01 -04:00 |
|
Soonho Kong
|
5c1d7458b5
|
fix(emacs/lean-input): fix input-method.js format
[skip ci]
|
2015-03-26 14:41:45 -04:00 |
|
Soonho Kong
|
c8e1ed9551
|
feat(emacs/lean-input): add lean-input-export-translations-to-stdout
|
2015-03-26 12:55:01 -04:00 |
|
Floris van Doorn
|
3d7656078d
|
feat(hott/types): prove that 'is_equiv f' is an hprop
|
2015-03-04 00:22:51 -05:00 |
|
Floris van Doorn
|
704f2b2697
|
feat(hott/algebra/category): prove that set is a univalent category assuming is_equiv is an hprop
|
2015-03-04 00:22:41 -05:00 |
|
Floris van Doorn
|
23a248ab28
|
style(hott): let inverse notation have higher binding power than application
|
2015-02-28 01:16:23 -05:00 |
|
Floris van Doorn
|
c091acc55b
|
feat(hott): remove funext as type class, add theorems to prove equalities between functors and natural transformations
|
2015-02-26 12:52:33 -05:00 |
|
Soonho Kong
|
cb83eca2f3
|
feat(emacs/lean-input): add lean-input-export-translations
|
2014-10-29 14:33:05 -07:00 |
|
Floris van Doorn
|
1612070350
|
feat(lean-input.el): add some new notation
|
2014-10-08 23:14:44 -07:00 |
|
Leonardo de Moura
|
1306d08399
|
feat(emacs/lean-input): add shortcuts for subscripts
|
2014-10-05 13:34:05 -07:00 |
|
Leonardo de Moura
|
f78d831de3
|
refactor(frontends/lean): remove hardcoded Type', and define it using notation
|
2014-10-02 14:29:51 -07:00 |
|
Leonardo de Moura
|
23960da532
|
feat(emacs/lean-input): shortcut for long arrow
|
2014-09-26 17:50:33 -07:00 |
|
Leonardo de Moura
|
3bbbd43b03
|
chore(emacs): minor adjustments to synthax hightlight and input mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-06 08:32:05 -07:00 |
|
Leonardo de Moura
|
359bfe93d5
|
feat(library/hott): add basic HoTT definitions and theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-15 21:46:33 +01:00 |
|
Leonardo de Moura
|
5e5ab1429d
|
feat(frontends/lean): parse and pretty print sigma types
This commit also fixes some bugs in the implementation of Sigma types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-03 18:16:00 -08:00 |
|
Leonardo de Moura
|
6fe362ef07
|
feat(emacs): include lean-mode Emacs files in the distribution
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-01-09 11:50:07 -08:00 |
|