Leonardo de Moura
|
a46abbb9ce
|
refactor(library/data): test new tactics in the standard library
|
2015-05-03 21:40:33 -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
|
75621df52b
|
feat(frontends/lean): uniform notation for lists in tactics
closes #504
|
2015-03-27 17:54:48 -07:00 |
|
Leonardo de Moura
|
bed0d6df6b
|
fix(frontends/lean/elaborator): inaccessible over coercion
|
2015-03-13 23:04:45 -07:00 |
|
Leonardo de Moura
|
27e58dc534
|
refactor(library/data): cleanup vector and list modules
|
2015-03-13 22:25:21 -07:00 |
|
Leonardo de Moura
|
167675a397
|
feat(library/data/vector): add nth and decidable_eq
|
2015-03-09 08:41:36 -07:00 |
|
Leonardo de Moura
|
a628836f28
|
feat(library/data/vector): add theorems
|
2015-03-08 22:51:11 -07:00 |
|
Leonardo de Moura
|
4fdac068b0
|
chore(library/data/vector): cleanup vector proofs
|
2015-03-06 17:37:03 -08:00 |
|
Leonardo de Moura
|
68110faa4d
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
Leonardo de Moura
|
5ca52d81ec
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
Leonardo de Moura
|
3ede8e9150
|
refactor(library): use [] binder annotation when declaring instances
|
2015-02-24 16:12:39 -08:00 |
|
Leonardo de Moura
|
05e1fc21f6
|
refactor(library/data/vector): define vector functions using recursive equations
|
2015-01-08 11:22:56 -08:00 |
|
Jeremy Avigad
|
6ad091d7bf
|
refactor(library): clean up headers and markdown files
|
2014-12-22 15:33:42 -05:00 |
|
Leonardo de Moura
|
7d19b5b743
|
refactor(library/data/vector): cleanup
|
2014-12-03 21:06:17 -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
|
5dc42762de
|
feat(library/data): define 'nat.addl' addition using recursion on the first argument, prove it to be equivalent to 'add', and use it to define vector.append
|
2014-11-17 22:03:39 -08:00 |
|
Leonardo de Moura
|
b5404cd979
|
refactor(library/data/vector): cleanup, use variables, add concat
|
2014-11-15 22:36:52 -08:00 |
|
Leonardo de Moura
|
85f24e4c80
|
feat(library/data/vector): add 'zip' and 'unzip' functions
|
2014-11-15 22:19:23 -08:00 |
|
Leonardo de Moura
|
a7adfde84f
|
feat(library/data/vector): use 'mechanical' definitions, and add 'last' function
The 'mechanical' definitions are "mimicking" what the definitional
package will do.
|
2014-11-15 20:21:18 -08:00 |
|
Leonardo de Moura
|
6bc89f0916
|
feat(library/definitional): define ibelow and below
These are helper definitions for brec_on and binduction_on
|
2014-11-12 16:38:46 -08:00 |
|
Leonardo de Moura
|
ef5a3e83ad
|
feat(library/data/vector): expand 'vector' module
|
2014-11-11 22:33:47 -08:00 |
|
Leonardo de Moura
|
777aa63660
|
fix(kernel/inductive): relax eliminator generation rules for empty types
This commit also removes the workaround false.rec_type. It is not needed anymore
|
2014-10-28 10:31:00 -07:00 |
|
Leonardo de Moura
|
cdcde661ef
|
feat(library/definitional/induction_on): automatically add 'induction_on'
|
2014-10-25 13:37:04 -07:00 |
|
Leonardo de Moura
|
a7a06ab0f8
|
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
|
2014-10-25 13:08:59 -07:00 |
|
Leonardo de Moura
|
e24225fabf
|
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
|
2014-10-21 15:39:47 -07:00 |
|
Leonardo de Moura
|
6c7e23ecaa
|
refactor(library): use 'reserve' notation in the standard library
|
2014-10-21 15:39:47 -07:00 |
|
Leonardo de Moura
|
8f1b6178a7
|
chore(*): minimize the use of parameters
|
2014-10-09 07:13:06 -07:00 |
|
Leonardo de Moura
|
4946f55290
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-10-02 17:55:34 -07:00 |
|
Leonardo de Moura
|
d42fd657fe
|
refactor(library): is_inhabited "theorems" should be "definitions", they are "data"
|
2014-10-02 09:00:34 -07:00 |
|
Leonardo de Moura
|
153e3927ac
|
feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type.
|
2014-10-01 18:50:17 -07:00 |
|
Leonardo de Moura
|
e64d5c4a4a
|
refactor(library/data/nat): use new operator '!'
|
2014-10-01 18:39:47 -07:00 |
|
Leonardo de Moura
|
716cd4d651
|
refactor(library): rename namespace eq_ops to eq.ops
|
2014-10-01 17:51:17 -07:00 |
|
Leonardo de Moura
|
86f06a54ea
|
refactor(library/data/vector): rename 'vec' to 'vector'
|
2014-09-19 16:20:50 -07:00 |
|
Leonardo de Moura
|
4e2377ddfc
|
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-19 15:54:32 -07:00 |
|
Leonardo de Moura
|
5d8c7fbdf1
|
refactor(frontends/lean): replace '[private]' modifier with 'private
definition' and 'private theorem', '[private]' is not a hint.
|
2014-09-19 15:54:32 -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
|
4e2f5572f3
|
feat(library/data/vector): add vec.is_inhabited theorem
|
2014-09-07 19:08:31 -07:00 |
|
Floris van Doorn
|
02d72e4c40
|
feat(library/data/category): add vector
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-05 09:57:04 -07:00 |
|