Jeremy Avigad
|
b68ce77650
|
refactor/feat(library/data/nat): fix up sub and div, rename theorems, add theorems
|
2015-01-13 11:56:25 -05:00 |
|
Jeremy Avigad
|
0dcf06000b
|
refactor(library/data/int/sub): rename theorems, add theorems, clean up
|
2015-01-12 16:28:42 -05:00 |
|
Leonardo de Moura
|
4f519be55e
|
fix(frontends/lean/elaborator): compilation problem
|
2015-01-11 20:58:41 -08:00 |
|
Leonardo de Moura
|
08a7997a97
|
refactor(library/data/string): put is_inhabited theorems on the toplevel
|
2015-01-10 14:07:20 -08:00 |
|
Leonardo de Moura
|
f053330755
|
refactor(library/data/sum): simplify has_decidable_eq proof using recursive equations and match expressions
|
2015-01-10 12:45:05 -08:00 |
|
Leonardo de Moura
|
75d7e4ab9e
|
feat(frontends/lean): add 'end' token to match expressions
|
2015-01-10 12:35:29 -08:00 |
|
Leonardo de Moura
|
d6eccd7c18
|
test(tests/lean/run): add match test
|
2015-01-10 10:43:24 -08:00 |
|
Leonardo de Moura
|
5796640392
|
fix(frontends/lean): do report unassigned metavariables in equation lhs
|
2015-01-10 10:39:47 -08:00 |
|
Leonardo de Moura
|
b172229a72
|
feat(frontends/lean): add 'match' expressions
We reuse the equations infrastructure to compile them.
|
2015-01-10 10:11:13 -08:00 |
|
Leonardo de Moura
|
6df9ffe5f6
|
fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler
|
2015-01-10 09:18:27 -08:00 |
|
Leonardo de Moura
|
a3bc1b0cd5
|
fix(library/definitional/equations): add more equation validation to avoid obscure error message
|
2015-01-09 18:52:21 -08:00 |
|
Leonardo de Moura
|
2e4a2451e6
|
refactor(library/reducible): simplify reducible/irreducible semantics
|
2015-01-08 18:52:18 -08:00 |
|
Leonardo de Moura
|
a23f3e9102
|
refactor(library/init/nat): use recursive equations to prove nat.has_decidable_eq
|
2015-01-08 12:38:44 -08:00 |
|
Leonardo de Moura
|
7a3a73d931
|
refactor(library/data/nat): move nat.comm_semiring to separate file
|
2015-01-08 12:12:30 -08:00 |
|
Leonardo de Moura
|
0ffb7c080f
|
fix(tests/lean/run/inv_bug2): adjust test to reflect changes at data.vector
|
2015-01-08 12:11:52 -08:00 |
|
Leonardo de Moura
|
698754b2bb
|
feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases
|
2015-01-08 12:00:47 -08:00 |
|
Leonardo de Moura
|
4fef19230d
|
feat(util/sexpr/options): add update_if_undef method
|
2015-01-08 11:55:30 -08:00 |
|
Leonardo de Moura
|
f344dd75c4
|
feat(library/pp_options): add get_pp_purify_locals_name
|
2015-01-08 11:55:08 -08:00 |
|
Leonardo de Moura
|
05e1fc21f6
|
refactor(library/data/vector): define vector functions using recursive equations
|
2015-01-08 11:22:56 -08:00 |
|
Leonardo de Moura
|
87d41e90fc
|
fix(frontends/lean/decl_cmds): store equations positions
|
2015-01-07 18:50:56 -08:00 |
|
Leonardo de Moura
|
4e49e73585
|
refactor(library/init/logic): add inhabited related functions, rename inhabited.default to default
|
2015-01-07 18:45:58 -08:00 |
|
Leonardo de Moura
|
1fab144aa7
|
refactor(library/init/nat): rename constants
closes #387
|
2015-01-07 18:26:51 -08:00 |
|
Jeremy Avigad
|
42c328e781
|
refactor(library/data/nat/basic): rename pred.zero and pred.succ
|
2015-01-07 18:18:28 -08:00 |
|
Jeremy Avigad
|
50f03c5a09
|
refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems
|
2015-01-07 18:18:28 -08:00 |
|
Leonardo de Moura
|
7b9758ac14
|
feat(library/data/fin): add of_nat_to_nat theorem
|
2015-01-07 17:46:47 -08:00 |
|
Leonardo de Moura
|
98412ee942
|
refactor(library/data/fin): redo fin using recursive equations
|
2015-01-07 17:38:00 -08:00 |
|
Leonardo de Moura
|
5c118127ae
|
fix(library/definitional/equations): memory access violation
|
2015-01-07 17:06:41 -08:00 |
|
Leonardo de Moura
|
597f7385e8
|
fix(library/unifier): incorrect fix
|
2015-01-07 16:57:02 -08:00 |
|
Leonardo de Moura
|
15b5344626
|
feat(library/definitional/equations): copy tags
|
2015-01-07 14:00:46 -08:00 |
|
Leonardo de Moura
|
4b47d22d05
|
refactor(library/data/list): use recursive equations
|
2015-01-07 13:38:11 -08:00 |
|
Leonardo de Moura
|
2990a6d029
|
fix(library/unifier): missing "set_conflict" in process_delta
|
2015-01-07 12:41:01 -08:00 |
|
Leonardo de Moura
|
a9b6e20a22
|
fix(frontends/lean): save equations position
|
2015-01-06 15:55:04 -08:00 |
|
Leonardo de Moura
|
760dc2162a
|
chore(library/definitional/equations): cleanup
|
2015-01-06 14:53:21 -08:00 |
|
Leonardo de Moura
|
a3a6697f44
|
feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes
|
2015-01-06 14:07:17 -08:00 |
|
Leonardo de Moura
|
fb1cb3c623
|
test(tests/lean/run): define tree_list length function using recursive equations
tree_list is part of a mutually inductive datatype.
|
2015-01-06 11:57:34 -08:00 |
|
Leonardo de Moura
|
559ee3e3e1
|
fix(util/buffer): bug in expand method
fixes #385
|
2015-01-06 11:42:40 -08:00 |
|
Leonardo de Moura
|
5f182dc1cc
|
fix(util/lean_path): memory leak
|
2015-01-06 10:22:45 -08:00 |
|
Leonardo de Moura
|
c33928f202
|
fix(library/pp_options): memory leak
|
2015-01-06 10:22:23 -08:00 |
|
Leonardo de Moura
|
6451cad38d
|
test(tests/lean/run): define list head using recursive equations
|
2015-01-05 19:50:34 -08:00 |
|
Leonardo de Moura
|
828ce3f8dc
|
feat(frontends/lean/decl_cmds): minor modifications for supporting mutually recursive functions
|
2015-01-05 19:23:50 -08:00 |
|
Leonardo de Moura
|
322cdb8a98
|
feat(library/definitional/equations): add 'equations_result' macro used to wrap multiple functions being defined by recursive equations
This is only useful when compiling "mutually recursive" functions.
|
2015-01-05 19:09:20 -08:00 |
|
Leonardo de Moura
|
3325d791de
|
fix(library/definitional/equations): bug in recursive application elimination
|
2015-01-05 17:17:14 -08:00 |
|
Leonardo de Moura
|
cbae6a2ca0
|
test(tests/lean/run): define list filter function using recursive equations
|
2015-01-05 17:05:01 -08:00 |
|
Leonardo de Moura
|
a24a7f7fa1
|
test(tests/lean/run) define vector last and unzip functions using recursive equations
|
2015-01-05 17:04:55 -08:00 |
|
Leonardo de Moura
|
eedc31f7e9
|
fix(library/definitional/equations): bug in "complete" transition
|
2015-01-05 16:27:29 -08:00 |
|
Leonardo de Moura
|
3889b60152
|
feat(library/definitional/equations): allow inductive datatype parameters in recursive equations
|
2015-01-05 15:56:28 -08:00 |
|
Leonardo de Moura
|
6eba4b4ac1
|
chore(library/definitional/equations): cleanup
|
2015-01-05 13:57:13 -08:00 |
|
Leonardo de Moura
|
d8f3bcec67
|
feat(library/init/logic): add 'arbitrary'
It is identical to default, but it is opaque.
That is, when we use 'arbitrary A', we cannot rely on the particular
value selected.
|
2015-01-05 13:27:09 -08:00 |
|
Leonardo de Moura
|
0d84943d52
|
test(tests/lean/run): show that nat has decidable equality using recursive equations
|
2015-01-05 12:41:18 -08:00 |
|
Leonardo de Moura
|
fd332e411d
|
test(tests/lean/run): add more overlapping patterns examples
|
2015-01-05 12:25:14 -08:00 |
|