Leonardo de Moura
c9132648a2
feat(CMakeLists): include HoTT library in binary package
2015-01-14 10:00:35 -08:00
Leonardo de Moura
91366c989d
test(tests/lean/run/finbug): add problematic definition test
2015-01-13 18:49:37 -08:00
Leonardo de Moura
ef529c660f
fix(library/definitional/no_confusion): mark no_confusion as reducible
...
Auxiliary definitions should be marked as reducible
2015-01-13 18:44:47 -08:00
Leonardo de Moura
e48df78938
feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs
...
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
2015-01-13 18:05:22 -08:00
Leonardo de Moura
8246feff67
refactor(library/logic/eq): cleanup proof
2015-01-13 17:12:21 -08:00
Leonardo de Moura
e4b9a89f5f
refactor(library/data/fin): remove unnecessary import
2015-01-13 16:35:59 -08:00
Leonardo de Moura
37e852ba61
feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs
2015-01-13 14:38:25 -08:00
Leonardo de Moura
e9338669dc
feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages
2015-01-13 13:30:12 -08:00
Leonardo de Moura
41935906a8
chore(frontends/lean): use update_if_undef
2015-01-13 13:02:14 -08:00
Leonardo de Moura
533438b011
chore(doc/authors): update
2015-01-13 12:25:38 -08:00
Leonardo de Moura
f90e6f9ae7
chore(doc/todo): update
2015-01-13 12:24:17 -08:00
Leonardo de Moura
7f0e5b3780
chore(README): remove link to obsolete page
2015-01-13 12:23:14 -08:00
Leonardo de Moura
0279070201
chore(README): add link to textbook
2015-01-13 12:21:08 -08:00
Leonardo de Moura
e5a8c67d22
fix(library/definitional/equations): assertion violation
2015-01-13 11:57:14 -08:00
Leonardo de Moura
1fbfe59a9a
feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line
...
closes #391
2015-01-13 11:14:44 -08:00
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
