Leonardo de Moura
|
2bb51554d5
|
feat(library/definitional/util): add telescope equality for HoTT library
This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.
|
2014-12-07 18:35:55 -08:00 |
|
Leonardo de Moura
|
6736f58548
|
refactor(library/definitional/util): cleanup
|
2014-12-07 16:41:28 -08:00 |
|
Leonardo de Moura
|
ec7f90cb16
|
feat(hott/init): make sure eq is universe polymorphic
Jakob and Floris needed path equality to be universe polymorphic when
proving univalence.
|
2014-12-06 09:43:42 -08:00 |
|
Leonardo de Moura
|
466b671752
|
fix(tests/lean/interactive/coe): adjust test to reflect changes in the standard library
|
2014-12-05 22:27:03 -08:00 |
|
Jeremy Avigad
|
057615532e
|
feat(library/data/int): replace int definition with structure and better computational behavior
|
2014-12-05 22:24:42 -08:00 |
|
Jakob von Raumer
|
133f935fce
|
fix(library/hott): issues resulting from merge
|
2014-12-05 22:21:49 -08:00 |
|
Jakob von Raumer
|
7c1b75c818
|
feat(library/hott): add proof that the type of nat trafos is a set
The characteriszation of nat trafo by sigma types up to equivalence is still to be done (two unsuccessful proof attempts included)
|
2014-12-05 22:21:36 -08:00 |
|
Jakob von Raumer
|
cc2de8a8d9
|
feat(library/hott): complete proof that object types of proper hott categories are one truncated
|
2014-12-05 22:21:31 -08:00 |
|
Jakob von Raumer
|
aad4592cad
|
feat(library/hott): complete theorems about truncatedness of isomorphism sets
|
2014-12-05 22:21:26 -08:00 |
|
Jakob von Raumer
|
5923392395
|
chore(library/hott): make precategory use the isomorphic structure
|
2014-12-05 22:21:21 -08:00 |
|
Jakob von Raumer
|
63afac301c
|
chore(library/hott): turn isomorphic into structure
|
2014-12-05 22:21:16 -08:00 |
|
Jakob von Raumer
|
dbce41114a
|
feat(library/hott): add definition of category
|
2014-12-05 22:21:12 -08:00 |
|
Jakob von Raumer
|
39ba9429f5
|
chore(library/hott): make constructions.lean compile, still lots of work to do
|
2014-12-05 22:21:06 -08:00 |
|
Jakob von Raumer
|
91862926e3
|
chore(library/hott): change precategory to structure, fix morphism.lean
|
2014-12-05 22:20:57 -08:00 |
|
Jakob von Raumer
|
6124b87870
|
fix(library/hott): adjust expliciteness of arguments
|
2014-12-05 22:20:51 -08:00 |
|
Jakob von Raumer
|
cda828bfe8
|
chore(library/algebra): change category to be a structure
|
2014-12-05 22:20:46 -08:00 |
|
Jakob von Raumer
|
b37a77d25e
|
chore(library/hott): move precategory definition to its own folder
|
2014-12-05 22:20:40 -08:00 |
|
Jakob von Raumer
|
9631c6b1a1
|
feat(library/hott): add iso_of_path lemma for precategories
|
2014-12-05 22:20:33 -08:00 |
|
Jakob von Raumer
|
a1b468d104
|
feat(library/hott): port a part of algebra/category/constructions.lean, slice category still to do
|
2014-12-05 22:20:25 -08:00 |
|
Jakob von Raumer
|
67f71ee376
|
feat(library/hott): finish porting of natural_transformation.lean
|
2014-12-05 22:20:18 -08:00 |
|
Jakob von Raumer
|
ae618c20fb
|
fix(library/hott): finish associativity proof
|
2014-12-05 22:20:11 -08:00 |
|
Jakob von Raumer
|
d8e2206bbc
|
feat(library/hott): try to replace the proof irrelevance
|
2014-12-05 22:19:50 -08:00 |
|
Jakob von Raumer
|
5fe8ee606f
|
feat(library/hott): port Floris' category implementation
|
2014-12-05 22:19:26 -08:00 |
|
Leonardo de Moura
|
93d5d43f71
|
fix(util/lean_path): typo
|
2014-12-05 22:15:07 -08:00 |
|
Leonardo de Moura
|
d09bc95eaf
|
feat(emacs): add Type0 highlight
|
2014-12-05 22:14:28 -08:00 |
|
Leonardo de Moura
|
94a825c472
|
feat(hott/init): add wf and prod to HoTT initialization
|
2014-12-05 21:48:08 -08:00 |
|
Leonardo de Moura
|
5e9ed30e7d
|
feat(hott/init/prod): show lex is well-founded in HoTT
|
2014-12-05 21:46:17 -08:00 |
|
Leonardo de Moura
|
cf7dd60442
|
feat(hott/init): add well-founded recursion to HoTT library
|
2014-12-05 21:36:34 -08:00 |
|
Leonardo de Moura
|
2306c14337
|
fix(ltags): support .hlean files
|
2014-12-05 16:26:05 -08:00 |
|
Leonardo de Moura
|
effbf78d36
|
fix(shell): use --server for .hlean files
|
2014-12-05 16:13:29 -08:00 |
|
Leonardo de Moura
|
53d6d76162
|
fix(frontends/lean/parser): generate error when 'exit' command is used
m_theorem_queue.join() method assumes there are no open namespaces/scopes
|
2014-12-05 16:12:23 -08:00 |
|
Leonardo de Moura
|
1dc0790004
|
feat(hott/init): add initialization files
|
2014-12-05 15:47:04 -08:00 |
|
Leonardo de Moura
|
d52fc83274
|
fix(build): clean-olean target should also clean HoTT library
|
2014-12-05 14:42:37 -08:00 |
|
Leonardo de Moura
|
0034ad9b34
|
feat(build): add HoTT library to build
|
2014-12-05 14:38:45 -08:00 |
|
Leonardo de Moura
|
eb87c18693
|
feat(*): add support for separate HoTT library
|
2014-12-05 14:34:02 -08:00 |
|
Leonardo de Moura
|
71e1555eb4
|
feat(emacs): use lean-mode for .hlean
|
2014-12-05 14:33:22 -08:00 |
|
Leonardo de Moura
|
e868ecce36
|
feat(frontends/lean): parse recursive equations
|
2014-12-04 17:03:21 -08:00 |
|
Leonardo de Moura
|
7a6d674b8e
|
refactor(frontends/lean/decl_cmds): cleanup definition_cmd
|
2014-12-04 16:03:29 -08:00 |
|
Leonardo de Moura
|
c8d8e7ac93
|
chore(library/definitional/equations): fix style
|
2014-12-04 16:00:33 -08:00 |
|
Leonardo de Moura
|
52334dca29
|
feat(frontends/lean): parse "decreasing" expressions
|
2014-12-04 15:11:23 -08:00 |
|
Leonardo de Moura
|
e267b2d120
|
feat(library/definitional/equations): add support for serializing equations
|
2014-12-04 15:11:18 -08:00 |
|
Leonardo de Moura
|
1d401ad862
|
feat(library/definitional): add "datastructure" for storing recursive equations
|
2014-12-04 12:39:59 -08:00 |
|
Leonardo de Moura
|
e72c4977f0
|
feat(frontends/lean): nicer notation for dependent if-then-else
|
2014-12-04 11:13:09 -08:00 |
|
Leonardo de Moura
|
ebda057499
|
fix(library/tactic/intros_tactic): seg fault at intros tactic, fixes #366
|
2014-12-04 09:26:10 -08:00 |
|
Leonardo de Moura
|
1a813fc720
|
test(tests/lean/run/nested_rec.lean): add nested recursion example based on well-founded recursion package
|
2014-12-03 22:11:01 -08:00 |
|
Leonardo de Moura
|
59d403f7d8
|
fix(library/tactic/inversion_tactic): warning on clang++
|
2014-12-03 21:14:10 -08:00 |
|
Leonardo de Moura
|
b6a1c118f4
|
fix(tests/lean/whnf): make sure the test does not produce 'sorry'
|
2014-12-03 21:12:33 -08:00 |
|
Leonardo de Moura
|
7d19b5b743
|
refactor(library/data/vector): cleanup
|
2014-12-03 21:06:17 -08:00 |
|
Leonardo de Moura
|
173e84c299
|
fix(tests/lean/struct_class): adjust test result to reflect recent changes
|
2014-12-03 20:32:33 -08:00 |
|
Floris van Doorn
|
e52157a8ea
|
feat(hott/types): start characterization of pi-types and W-types
|
2014-12-03 20:29:16 -08:00 |
|