Leonardo de Moura
3d63c0b5dc
refactor(library/algebra/ring): using new structure instance syntax sugar to define instance
2015-01-16 17:42:30 -08:00
Leonardo de Moura
a86661f42c
refactor(library/algebra/ordered_group): using new structure instance syntax sugar to define instances
2015-01-16 17:37:08 -08:00
Leonardo de Moura
ebc1878028
refactor(library/algebra/group): using new structure instance syntax sugar to define instances
2015-01-16 17:23:41 -08:00
Leonardo de Moura
f9d7480f5c
feat(frontends/lean): notation for creating structure instances
2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d
feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields
...
See new test for an example.
closes #371
2015-01-16 13:04:48 -08:00
Leonardo de Moura
13660cfecd
feat(frontends/lean/parser): add parse_qualified_expr
2015-01-16 12:42:42 -08:00
Leonardo de Moura
6c07ca5d41
perf(library/print): improve is_used_name
2015-01-15 19:01:13 -08:00
Leonardo de Moura
c6290f01d0
perf(kernel/free_vars): improve has_free_var
2015-01-15 18:42:56 -08:00
Leonardo de Moura
f397da111a
perf(kernel/error_msgs): avoid unnecessary work
2015-01-15 18:32:52 -08:00
Leonardo de Moura
ce0b1d17a2
perf(kernel/free_vars): improve has_free_var
2015-01-15 18:31:43 -08:00
Leonardo de Moura
ddcc8de09e
fix(shell/lean): catch errors when loading bad cache file
2015-01-15 18:06:22 -08:00
Leonardo de Moura
30817aa2b1
feat(emacs): allow user to provide extra commands to lean-server
2015-01-15 16:54:55 -08:00
Leonardo de Moura
84715c12eb
feat(linja): add '-M' and '-T' options to linja
2015-01-15 16:54:55 -08:00
Leonardo de Moura
907f90096e
feat(kernel): add memory consumption checks at replace_fn and for_each_fn
2015-01-15 16:54:55 -08:00
Leonardo de Moura
8ab775bd6f
feat(*): distinguish between logical and runtime exceptions.
...
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
2015-01-15 16:54:55 -08:00
Leonardo de Moura
3a865e95fe
feat(shell/lean): add option '-M' to limit amount of memory consumed
2015-01-15 16:54:55 -08:00
Leonardo de Moura
5c9a277dea
feat(CMakeLists): include runtime files in Windows binary distribution package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2015-01-14 12:37:25 -08:00
Leonardo de Moura
1c176fd06d
feat(doc/bin/README): add link to documentation
2015-01-14 10:42:39 -08:00
Leonardo de Moura
730e038dd3
feat(CMakeLists): add basic example to binary distribution package
2015-01-14 10:39:07 -08:00
Leonardo de Moura
0509baa64a
feat(CMakeLists): add README file for binary distribution packages
2015-01-14 10:35:51 -08:00
Leonardo de Moura
ee98523c2a
feat(shell/lean): add option '-T' alias for '-t 1025'
2015-01-14 10:21:57 -08:00
Leonardo de Moura
3813aeede5
fix(util/lean_path): relative position of library files in binary
...
distribution packages
2015-01-14 10:14:17 -08:00
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
