Leonardo de Moura
|
73429547ba
|
fix(init/reserved_notation): remove "invisible" character at \/
|
2014-12-02 12:06:39 -08:00 |
|
Leonardo de Moura
|
06f436840f
|
fix(library/unifier): postpone class-instance constraints whose type could not be inferred
|
2014-12-01 22:27:23 -08:00 |
|
Leonardo de Moura
|
e6672b958f
|
fix(library/tactic/inversion_tactic): add missing case
|
2014-12-01 19:11:44 -08:00 |
|
Leonardo de Moura
|
b094c1cf43
|
refactor(library/init): move num->nat coercion to init
|
2014-12-01 08:23:31 -08:00 |
|
Leonardo de Moura
|
5d4b6a3de2
|
chore(library/logic/logic.md): adjust documentation
|
2014-11-30 21:19:56 -08:00 |
|
Leonardo de Moura
|
697d4359e3
|
refactor(library): add 'init' folder
|
2014-11-30 20:34:12 -08:00 |
|
Leonardo de Moura
|
8dfd22e66c
|
feat(frontends/lean): add 'prelude' command, and init directory
|
2014-11-30 17:03:08 -08:00 |
|
Leonardo de Moura
|
7dc055cfc9
|
chore(library/data/nat/decl): remove leftover
|
2014-11-30 15:10:10 -08:00 |
|
Leonardo de Moura
|
dad94eafbe
|
refactor(data/nat/decl): use new naming convention at data/nat/decl.lean
|
2014-11-30 15:07:09 -08:00 |
|
Leonardo de Moura
|
f24eed50af
|
refactor(library/logic/heq): minor change
|
2014-11-30 13:52:34 -08:00 |
|
Leonardo de Moura
|
c08f4672e4
|
feat(library/tactic): add 'assert' tactic, closes #349
|
2014-11-29 21:34:49 -08:00 |
|
Leonardo de Moura
|
1a7dd56f0f
|
fix(library/tools/tactic): 'cases' argument precedence
|
2014-11-29 21:03:45 -08:00 |
|
Leonardo de Moura
|
f51fa93292
|
feat(library/tactic): add 'fapply' tactic, closes #356
|
2014-11-29 19:20:41 -08:00 |
|
Leonardo de Moura
|
2281fb30c8
|
refactor(library): use "symbolic" precedences in the standard library
|
2014-11-29 19:08:37 -08:00 |
|
Leonardo de Moura
|
2c0472252e
|
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
|
2014-11-29 18:29:48 -08:00 |
|
Leonardo de Moura
|
bed9467315
|
chore(library/hott/trunc): remove set_option
|
2014-11-29 08:55:47 -08:00 |
|
Leonardo de Moura
|
d7042c4618
|
fix(library/logic/heq): heq.to_eq must be transparent because it is needed in the 'inversion' tactic used by definitional package
|
2014-11-28 23:49:17 -08:00 |
|
Leonardo de Moura
|
cab99e2e22
|
refactor(library/data/vector): simplify 'vector' using new 'inversion' tactic
|
2014-11-28 23:19:53 -08:00 |
|
Leonardo de Moura
|
ae0daf9639
|
fix(library/data/prod/decl): give preference to unicode version when pretty printing
|
2014-11-28 23:02:19 -08:00 |
|
Jeremy Avigad
|
a9001166fd
|
fix(library/algebra/category/morphism): remove sorry that was introduced by accident
|
2014-11-28 22:54:15 -08:00 |
|
Jeremy Avigad
|
bb8d436e75
|
refactor(library/algebra/relation, library/logic/instances): revise equivalence relations and congruences to use structure command
|
2014-11-28 22:54:15 -08:00 |
|
Jeremy Avigad
|
7571f50870
|
feat(library/binary, library/relation): introduce general properties for binary operations and relations
|
2014-11-28 22:54:15 -08:00 |
|
Jeremy Avigad
|
89380f088e
|
feat(library): reorganize and declare some notation
|
2014-11-28 22:54:15 -08:00 |
|
Jeremy Avigad
|
58e325f0af
|
feat(library/algebra): add to developments of group, ordered_group, and ring
|
2014-11-28 22:54:15 -08:00 |
|
Jeremy Avigad
|
f923d6a24c
|
feat(library/data/sum): use + notation for sum
|
2014-11-28 22:54:15 -08:00 |
|
Jakob von Raumer
|
7c81044a99
|
chore(library/hott) change is_pointed to structure
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
0417c21bbb
|
chore(library/hott) change naming in equiv_precomp
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
4587e46c67
|
chore(library/hott) change naming to leo's naming proposal
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
7374149758
|
chore(library/hott) change equiv.lean to use structures and more typeclass inference
|
2014-11-28 22:50:43 -08:00 |
|
Leonardo de Moura
|
011e955fed
|
refactor(library/data/fin): simplify 'fin' module using new inversion tactic
|
2014-11-28 22:46:06 -08:00 |
|
Leonardo de Moura
|
e0debca771
|
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
|
2014-11-28 22:25:37 -08:00 |
|
Leonardo de Moura
|
c2602baf2b
|
feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic
|
2014-11-28 19:33:11 -08:00 |
|
Leonardo de Moura
|
ebd320a6b3
|
feat(library/tactic): add first step of 'inversion' tactic
|
2014-11-26 21:28:00 -08:00 |
|
Leonardo de Moura
|
f7deabfd19
|
feat(library/rename): add notation for rename
|
2014-11-26 19:02:11 -08:00 |
|
Leonardo de Moura
|
e55397d422
|
feat(library/tactic): add 'clears' and 'reverts' variants
|
2014-11-26 14:49:48 -08:00 |
|
Leonardo de Moura
|
2bd8f969d5
|
feat(library/tactic): add 'revert' tactic, closes #346
|
2014-11-26 14:23:42 -08:00 |
|
Leonardo de Moura
|
df51ba8b7c
|
feat(library/definitional/projection): use strict implicit inference, closes #344
|
2014-11-25 18:04:06 -08:00 |
|
Jakob von Raumer
|
53d66c91fc
|
chore(library/hott) made ua_implies_funext a class instance
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
757cdcb130
|
feat(library/hott) funext from ua now with arbitrary universe levels for funext!
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
228205634d
|
chore(library/hott) make funext more general
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
12429c93c8
|
fix(library/hott) fix equiv_precomp, doesn't look nice now
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
1f6b6ff8e6
|
chore(library/hott) adjust funext_from_ua.lea to typeclass axioms
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
2d9621892b
|
fix(library/hott) fill both gaps (I don't know why it works that way), change name from funext.apply to funext.ap, since apply seems to be a tactic name?
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
fd47a162de
|
chore(library/hott) adapted theories to typeclass axioms
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
d8d2ea998d
|
feat(library/hott) change axioms to Leo's axioms-as-typeclass proposal
|
2014-11-23 17:43:55 -08:00 |
|
Leonardo de Moura
|
64686c1278
|
feat(frontends/lean): allow user to associate precedence to binders, closes #323
|
2014-11-23 17:30:46 -08:00 |
|
Leonardo de Moura
|
7231a36ec7
|
refactor(library/data/nat/div): remove unnecessary annotations
|
2014-11-23 17:30:46 -08:00 |
|
Leonardo de Moura
|
13fba433b0
|
feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
|
2014-11-23 17:30:22 -08:00 |
|
Floris van Doorn
|
3523a70b4c
|
fix(hott/path): make recursion-like definitions reducible
|
2014-11-22 17:44:13 -08:00 |
|
Floris van Doorn
|
e97b0b4e8e
|
feat(hott/types): port more of the sigma library from Coq
prove theorems about interaction of sigma types and n-types, including the fact that sigmas preserve n-types
|
2014-11-22 17:44:12 -08:00 |
|