Leonardo de Moura
|
3cd8f38b8d
|
feat(library/data/string): prove that string and char have decidable equality
|
2015-05-03 21:08:09 -07:00 |
|
Leonardo de Moura
|
4e1146a2d5
|
refactor(hott,library): test new tactics in the HoTT and standard libraries
|
2015-05-02 22:22:31 -07:00 |
|
Leonardo de Moura
|
b39fe17dee
|
feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics
closes #500
|
2015-05-02 15:48:25 -07:00 |
|
Leonardo de Moura
|
cd17618f4a
|
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
|
2015-05-02 15:15:35 -07:00 |
|
Leonardo de Moura
|
415ca2b93f
|
feat(library/tactic): add 'congruence' tactic
It is the f_equal described at issue #500.
|
2015-05-02 12:58:46 -07:00 |
|
Leonardo de Moura
|
458d13025f
|
refactor(library,hott): define 'congr' in the initialization files
|
2015-05-02 11:29:31 -07:00 |
|
Leonardo de Moura
|
ac8ba6a3cf
|
feat(library/tactic): add 'subst' tactic
see issue #500
|
2015-05-01 19:31:24 -07:00 |
|
Leonardo de Moura
|
e8affed020
|
refactor(library): test new tactics in the standard library
|
2015-05-01 18:18:29 -07:00 |
|
Leonardo de Moura
|
de369a0a0a
|
feat(library/tactic/injection_tactic): improve 'injection' tactic
see issue #500
|
2015-05-01 15:49:56 -07:00 |
|
Leonardo de Moura
|
9ba8b284a1
|
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
|
2015-05-01 15:08:00 -07:00 |
|
Leonardo de Moura
|
e948dd239c
|
feat(library/data/list/perm): use new 'injection' tactic
|
2015-05-01 13:08:36 -07:00 |
|
Leonardo de Moura
|
63eb155c7e
|
feat(library/tactic): add 'injection' tactic
see issue #500
|
2015-05-01 12:45:21 -07:00 |
|
Leonardo de Moura
|
1e18a76bdb
|
chore(library/init/nat): replace 'no_confusion' with 'by contradiction'
|
2015-04-30 21:26:52 -07:00 |
|
Leonardo de Moura
|
2d9c950144
|
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
see issue #500
|
2015-04-30 21:15:07 -07:00 |
|
Leonardo de Moura
|
d152f38518
|
feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics
see issue #500
|
2015-04-30 17:52:29 -07:00 |
|
Leonardo de Moura
|
1c6067bac2
|
feat(library/tactic): add 'exfalso' tactic
see issue #500
|
2015-04-30 15:43:07 -07:00 |
|
Leonardo de Moura
|
59b11c815c
|
refactor(library/data/list/perm): remove unnessary lambda abstractions
The contradiction tactic takes care of it.
|
2015-04-30 14:02:19 -07:00 |
|
Leonardo de Moura
|
9760968b45
|
refactor(library,hott): use/test new 'contradiction' tactic in the standard and hott libraries
|
2015-04-30 13:56:12 -07:00 |
|
Leonardo de Moura
|
9c8a63caec
|
feat(library/tactic): add 'contradiction' tactic
see issue #500
Remark: this tactic also applies no_confusion to take care of a contradiction
|
2015-04-30 13:47:40 -07:00 |
|
Leonardo de Moura
|
3233008039
|
feat(library/tactic): allow user to name generalized term in the 'generalize' tactic
closes #421
|
2015-04-30 11:57:40 -07:00 |
|
Leonardo de Moura
|
3912bc24c8
|
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
|
2015-04-30 11:00:39 -07:00 |
|
Leonardo de Moura
|
f60dc8ae8f
|
refactor(library/init/nat): cleanup
|
2015-04-30 10:10:13 -07:00 |
|
Leonardo de Moura
|
018f768555
|
chore(library): remove some unnecessary parentheses
|
2015-04-29 14:39:59 -07:00 |
|
Leonardo de Moura
|
d2c7b5c319
|
feat(library/tactic): add 'let' tactic
closes #555
|
2015-04-28 17:24:43 -07:00 |
|
Leonardo de Moura
|
a23118d357
|
feat(frontends/lean): add tactic_notation command
This addresses the first part of issue #461
We still need support for tactic definitions
|
2015-04-27 17:46:13 -07:00 |
|
Leonardo de Moura
|
ca8943f45b
|
feat(library,hott): remove rapply tactic
|
2015-04-27 15:06:16 -07:00 |
|
Leonardo de Moura
|
17c07cdb02
|
feat(library/data/rat/order): define abs and sign for rat before migrate
|
2015-04-27 12:59:02 -07:00 |
|
Jeremy Avigad
|
7a1064b7e8
|
refactor(library/algebra/order.lean): rename a field in an order structure
|
2015-04-27 12:03:41 -07:00 |
|
Jeremy Avigad
|
d8e40d90d6
|
feat(library/data/rat/order.lean): make rat a linear ordered field
|
2015-04-27 12:03:41 -07:00 |
|
Leonardo de Moura
|
76c773ad3d
|
feat(library/data/examples/depchoice): add dependent choice example
|
2015-04-26 12:56:23 -07:00 |
|
Leonardo de Moura
|
072bf0b3b4
|
refactor(library): make sure "choose" compute inside the kernel
|
2015-04-25 23:10:48 -07:00 |
|
Leonardo de Moura
|
d455bb4c5b
|
feat(library/data/fintype): add decidable_exists_finite
|
2015-04-25 21:38:03 -07:00 |
|
Leonardo de Moura
|
6bb6644c25
|
feat(library/data/squash): define squash type using quotients
|
2015-04-24 18:11:25 -07:00 |
|
Leonardo de Moura
|
9d01868361
|
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
closes #502
|
2015-04-24 17:23:12 -07:00 |
|
Leonardo de Moura
|
1149ead14c
|
chore(library/logic/examples/colog88): remove unnecessary annotation
|
2015-04-24 12:45:06 -07:00 |
|
Leonardo de Moura
|
a5306e70eb
|
feat(library/logic/examples/negative): add example showing that allowing negative inductive datatypes would lead to inconsistency
|
2015-04-24 09:33:09 -07:00 |
|
Leonardo de Moura
|
15c331591e
|
feat(library/logic/examples/colog88): add example from COLOG-88 paper
|
2015-04-24 09:33:09 -07:00 |
|
Leonardo de Moura
|
2613e7c444
|
fix(frontends/lean): bug when handling identifiers in tactics
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
|
2015-04-22 16:03:22 -07:00 |
|
Floris van Doorn
|
9d805437f0
|
fix(reserved_notation): lower binding power of 'iff'
|
2015-04-22 13:06:11 -07:00 |
|
Leonardo de Moura
|
670eac9d50
|
refactor(library): avoid 'context' command in the standard library
|
2015-04-21 19:13:19 -07:00 |
|
Leonardo de Moura
|
bf8a7eb9b4
|
fix(library/scoped_ext): bug in local metadata in sections
The problem is described in issue #554
|
2015-04-21 18:56:28 -07:00 |
|
Leonardo de Moura
|
6f6d106a10
|
feat(library/tactic): add "check_expr" tactic
closes #486
|
2015-04-19 19:00:05 -07:00 |
|
Leonardo de Moura
|
306087b5d3
|
refactor(library/data): rename 'countable' to 'encodable', define countable in the usual way, and prove all 'encodable' type is 'countable'
|
2015-04-19 14:20:47 -07:00 |
|
Jeremy Avigad
|
f4398115b4
|
feat(library/data/rat/basic.lean): begin theory of rationals, show rat is a field
|
2015-04-18 11:39:52 -07:00 |
|
Jeremy Avigad
|
6359132b67
|
refactor(library/algebra/field.lean): rename has_decidable_eq and declare instance
|
2015-04-18 11:39:52 -07:00 |
|
Jeremy Avigad
|
dfaeb475cc
|
feat(library/init/reserved_notation.lean): add equiv relation symbol
|
2015-04-18 11:39:52 -07:00 |
|
Jeremy Avigad
|
5eb7fef564
|
feat(library/algebra/order.lean, data/int/{basic,order}.lean): add theorem, correct gt_trans
|
2015-04-18 11:39:52 -07:00 |
|
Jeremy Avigad
|
53919699bc
|
refactor(library/logic/axioms/prop_decidable.lean): simplify proof of prop_decidable (using arbitrary instead of epsilon)
|
2015-04-18 11:39:52 -07:00 |
|
Leonardo de Moura
|
cc63a40a01
|
feat(library): enforce name conventions on old nat declarations
|
2015-04-18 10:50:30 -07:00 |
|
Leonardo de Moura
|
10954a073c
|
feat(library/logic/examples): add new example from Martín Escardó paper
|
2015-04-17 15:22:52 -07:00 |
|