Leonardo de Moura
|
128b557d37
|
refactor(frontends/lean): use attribute_manager to simplify decl_attributes
|
2015-12-17 22:28:53 -08:00 |
|
Floris van Doorn
|
74366aa061
|
fix(hott): change some theorems to definitions
This ensures that the HoTT library compiles with the option --to_axiom
|
2015-12-17 12:46:16 -08:00 |
|
Floris van Doorn
|
c852f7bc71
|
feat(hott): use the induction tactic for trunc at some places
|
2015-12-17 12:46:16 -08:00 |
|
Floris van Doorn
|
da5f10ce63
|
feat(hott): minor fixes. allow the usage of numerals for trunc_index
|
2015-12-17 12:46:16 -08:00 |
|
Leonardo de Moura
|
61ecf018e9
|
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
|
2015-12-17 12:18:32 -08:00 |
|
Leonardo de Moura
|
c824a0e050
|
chore(library,hott): enforce naming conventions
|
2015-12-17 11:36:58 -08:00 |
|
Leonardo de Moura
|
13419d1561
|
chore(hott/library): cleanup
|
2015-12-17 11:31:07 -08:00 |
|
Sebastian Ullrich
|
2185ee7e95
|
feat(library/tactic): make let tactic transparent, introduce new opaque note tactic
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
|
2015-12-14 10:14:02 -08:00 |
|
Leonardo de Moura
|
e3a35ba4fd
|
feat(frontends/lean): add 'with_attributes' tactical
closes #494
|
2015-12-13 18:27:44 -08:00 |
|
Leonardo de Moura
|
d4e49a8434
|
feat(library/tactic/intros_tactic): intro without argument should introduce a single variable
see #695
|
2015-12-13 16:28:39 -08:00 |
|
Floris van Doorn
|
4ef58f1ba5
|
chore(hott): more cleanup.
Make zero and one reducible (see algebra/port.md)
Change some theorems which need to compute into definitions
|
2015-12-10 10:42:16 -08:00 |
|
Floris van Doorn
|
c968f920ba
|
chore(hott): cleanup
|
2015-12-10 10:42:16 -08:00 |
|
Floris van Doorn
|
65c93b180d
|
fix(types.md): add num
|
2015-12-09 12:36:11 -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 |
|
Floris van Doorn
|
14a2c8e444
|
fix(init/nat): add spaces around inequalities
|
2015-12-09 12:34:06 -08:00 |
|
Floris van Doorn
|
377755e5ab
|
feat(types/sigma): add lemma
|
2015-12-09 12:34:06 -08:00 |
|
Leonardo de Moura
|
6404c3c014
|
chore(hott/types/nat/order): remove occurrence of "migrate" command
|
2015-12-08 15:37:13 -08:00 |
|
Leonardo de Moura
|
85379b7706
|
feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled
not (not (not a)) -> not a
|
2015-12-07 09:30:14 -08:00 |
|
Jakob von Raumer
|
cc8a5581d6
|
chore(hott/cubical): add lost space hints around square concatenations
|
2015-12-02 23:13:25 -08:00 |
|
Jakob von Raumer
|
68901c7788
|
feat(hott/homotopy): complete join associativity proof, helper lemmas for squares
|
2015-12-02 23:13:21 -08:00 |
|
Jakob von Raumer
|
bd064ef9c8
|
feat(hott/homotopy): prove missing helper lemmas up to cube massaging
|
2015-12-02 23:13:17 -08:00 |
|
Jakob von Raumer
|
811f3067ff
|
feat(hott): join associativity proof done up to small auxiliary lemmas, add transposition, inversion of cubes
|
2015-12-02 23:13:12 -08:00 |
|
Jakob von Raumer
|
1d68d57bb9
|
chore(hott/cubical): adapt cubovers to new order of faces
|
2015-12-02 23:13:07 -08:00 |
|
Jakob von Raumer
|
e481e541a2
|
feat(hott/homotopy): more progress on join associativity
|
2015-12-02 23:13:03 -08:00 |
|
Jakob von Raumer
|
6c6dde7e48
|
feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed
|
2015-12-02 23:12:59 -08:00 |
|
Jakob von Raumer
|
1b52ae8858
|
feat(hott/cubical): add cube concatenations
|
2015-12-02 23:12:54 -08:00 |
|
Jakob von Raumer
|
3f1cf3835f
|
chore(hott/cubical): change order of visible arguments in cube
|
2015-12-02 23:12:50 -08:00 |
|
Jakob von Raumer
|
54b1d1a9fe
|
feat(hott/homotopy): more steps towards join associativity, cube composition
|
2015-12-02 23:12:46 -08:00 |
|
Jakob von Raumer
|
e1e8680474
|
feat(hott/homotopy): continue defining squares for join associativity
|
2015-12-02 23:12:41 -08:00 |
|
Jakob von Raumer
|
2bc45f4de1
|
feat(hott/cubical): add cubes which are degenerate in one dimension
|
2015-12-02 23:12:37 -08:00 |
|
Jakob von Raumer
|
bba6ab5a6d
|
feat(hott/cubical): add fillers and other little lemmas for squares and cubes
|
2015-12-02 23:12:34 -08:00 |
|
Jakob von Raumer
|
12a498d411
|
feat(hott/homotopy): add join switch and derive associativity from switch
|
2015-12-02 23:12:29 -08:00 |
|
Jakob von Raumer
|
149e5fff9f
|
feat(hott/homotopy): add commutativity proof for join
|
2015-12-02 23:12:24 -08:00 |
|
Jakob von Raumer
|
eea219e33f
|
feat(hott/homotopy): start associativity proof for join
|
2015-12-02 23:12:19 -08:00 |
|
Floris van Doorn
|
c44ad80e4e
|
feat(homotopy/torus): give recursion and induction principle for the torus
also change the surface of the torus to a square instead of an equality between paths
|
2015-11-22 18:29:37 -08:00 |
|
Floris van Doorn
|
fe8a858d79
|
feat(hott): add recursor to refl_quotient
|
2015-11-22 18:29:37 -08:00 |
|
Floris van Doorn
|
ae92e8c94d
|
feat(hit/two_quotient): give dependent eliminator for two_quotients
|
2015-11-22 18:29:37 -08:00 |
|
Floris van Doorn
|
0537ef2bd9
|
chore(*): add me as author to files where I made nontrivial contributions
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
74aff044ef
|
feat(group): port three more theorems from the standard library
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
482c68b387
|
feat(*/list): add some computation rules for lists in both libraries
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
93283a4cf8
|
feat(list): also port part of list.comb
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
cc03ca9c6d
|
fix(reserved_notation): make :: bind stronger than ++
this allows us to write l1 ++ a :: l2 without parentheses
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
5abc450fad
|
feat(list): port list.basic from the standard library
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
88a62f8e74
|
feat(algebra|types): small additions
add to markdown file for algebra, and add some definitions in types/
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
5328486d49
|
feat(hit): add elimination rule to propositions
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
5b8486a34f
|
feat(set_quotient): add some properties for set_quotients
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
45d808ce7f
|
feat(homotopy/circle): give all higher homotopy groups of the circle
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
810a399699
|
style(homotopy/circle): clean-up encode-decode proof
|
2015-11-22 14:21:25 -08:00 |
|
Leonardo de Moura
|
491c7c55e1
|
feat(library/simplifier/simp_rule_set): add priorities for simp and congr rules
|
2015-11-16 22:34:06 -08:00 |
|