Floris van Doorn
|
cd33d2e96d
|
refactor(typeof): move typeof to general_notation
|
2014-11-08 19:12:54 -08:00 |
|
Floris van Doorn
|
74779dd855
|
feat(hott/trunc): clean up some theorems, prove some basic theorems
|
2014-11-08 19:12:54 -08:00 |
|
Floris van Doorn
|
08c56188b6
|
feat(library/hott/trunc): prove that n-types are (n+1)-types.
|
2014-11-08 19:12:54 -08:00 |
|
Leonardo de Moura
|
6b89080b1a
|
feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248
|
2014-10-21 16:28:36 -07:00 |
|
Leonardo de Moura
|
98e66586e9
|
feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit
|
2014-10-02 14:29:51 -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
|
38a4852e7d
|
feat(library/hott): add 'path' namespace
|
2014-09-09 14:03:45 -07:00 |
|
Leonardo de Moura
|
364bba2129
|
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 17:26:36 -07:00 |
|
Leonardo de Moura
|
8743394627
|
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 15:04:57 -07:00 |
|
Leonardo de Moura
|
dbaf81e16d
|
refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-23 18:08:09 -07:00 |
|