Gabriel Ebner
|
7353a54aac
|
fix(library/vm/vm): prevent segfault
|
2017-05-18 09:41:31 -07:00 |
|
Gabriel Ebner
|
d9f5e0bb1f
|
fix(library/app_builder): prevent segfault
|
2017-05-18 09:41:31 -07:00 |
|
Gabriel Ebner
|
4528711efb
|
fix(library/type_context): prevent segfault
Temporary metavariables appeared here when pretty-printing simp_lemmas.
|
2017-05-18 09:41:31 -07:00 |
|
Sebastian Ullrich
|
9b86808345
|
fix(frontends/lean/structure_cmd): parent structures may use different universe params
Fixes #1585
|
2017-05-18 09:35:14 -07:00 |
|
Sebastian Ullrich
|
9fdf11fa54
|
fix(frontends/lean/pp): shadowing shortened const
Fixes #1584
|
2017-05-18 09:35:14 -07:00 |
|
Leonardo de Moura
|
737136e8fd
|
feat(library/equations_compiler/wf_rec): apply well_founded.fix
|
2017-05-17 16:44:53 -07:00 |
|
Leonardo de Moura
|
7cf848cbb2
|
chore(tests/lean/run/wfrec1): cleanup example
|
2017-05-17 16:06:45 -07:00 |
|
Leonardo de Moura
|
4982e23dca
|
feat(library/equations_compiler/wf_rec): eliminate recursive calls using functional
|
2017-05-17 15:56:53 -07:00 |
|
Leonardo de Moura
|
56823a22b7
|
feat(library/equations_compiler/wf_rec): use has_well_founded type class to generate default well founded relation when one is not provided
|
2017-05-17 14:37:21 -07:00 |
|
Leonardo de Moura
|
499fc355df
|
feat(library/init): add has_well_founded type class
|
2017-05-17 14:34:52 -07:00 |
|
Leonardo de Moura
|
1c87319b58
|
feat(library/equations_compiler): add wf_rec skeleton
|
2017-05-17 12:47:52 -07:00 |
|
Leonardo de Moura
|
dea8a856dc
|
chore(library/equations_compiler/compiler): generate error when using well founded recursion in meta definitions
|
2017-05-17 12:24:47 -07:00 |
|
Sebastian Ullrich
|
75786e9a6e
|
feat(frontends/lean/pp): hide (some) defaulted arguments on pp.implicit true
|
2017-05-17 10:38:12 -07:00 |
|
Sebastian Ullrich
|
84997bf4de
|
refactor(init/meta/expr): unify expr and pexpr
|
2017-05-17 10:38:12 -07:00 |
|
Sebastian Ullrich
|
aefd312a98
|
feat(frontends/lean/decl_util): allow opt_param shorthand in all decls
|
2017-05-17 10:38:12 -07:00 |
|
Sebastian Ullrich
|
5f3e0a1cc4
|
feat(frontends/lean/decl_cmds): allow implicit locals in constants & axioms
|
2017-05-17 10:38:12 -07:00 |
|
Leonardo de Moura
|
cb6d5675df
|
chore(library/init): ^. ==> .
|
2017-05-16 15:00:58 -07:00 |
|
Leonardo de Moura
|
7d2ec25e81
|
fix(tests/lean/interactive/complete_field): fix tests
|
2017-05-16 14:50:15 -07:00 |
|
Leonardo de Moura
|
cba0eef101
|
fix(library/data, library/init/data/array): adjust hash_map PR
|
2017-05-16 14:46:43 -07:00 |
|
Mario Carneiro
|
422820243d
|
chore(tools/super/utils): remove duplicate partition def
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
6b28499e47
|
feat(init/data/list,data/list): new basic list operations from haskell
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
7257e32eca
|
refactor(init/data/list/lemmas): remove projection notation
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
69c2c998a7
|
fix(init/data/list/lemmas): fix references to drop
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
19a919061f
|
fix(library/data/hash_map): respond to review comments
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
5d89a93fce
|
feat(library/data/hash_map): verified hash_map
|
2017-05-16 14:38:43 -07:00 |
|
Mario Carneiro
|
3b89739850
|
feat(library/data/list, library/data/array): theorems needed for new hash_map
Note that hash_map is moved to library_dev, where the more advanced theorems on lists are available
|
2017-05-16 14:38:43 -07:00 |
|
Leonardo de Moura
|
ed6b7662df
|
feat(library/init/data): add aux lemmas
|
2017-05-16 14:25:06 -07:00 |
|
Leonardo de Moura
|
8b32f3e7a9
|
chore(library/init/data/fin/basic): pretty print fin.mk using anonymous constructor notation
|
2017-05-16 13:54:12 -07:00 |
|
Leonardo de Moura
|
0091cef9f2
|
feat(library/tactic): start algebraic normalizer
|
2017-05-15 21:46:19 -07:00 |
|
Leonardo de Moura
|
eddc5b0869
|
chore(kernel/environment): rename method
|
2017-05-15 14:18:16 -07:00 |
|
Leonardo de Moura
|
4575c9e038
|
feat(frontends/lean): swap (t) and ``(t) semantics
|
2017-05-15 09:41:31 -07:00 |
|
Leonardo de Moura
|
76ff23c154
|
chore(tests/lean): fix tests
|
2017-05-14 19:40:36 -07:00 |
|
Mario Carneiro
|
7ace147f25
|
refactor(init/meta/tactic): replace assertv -> note, definev -> pose
|
2017-05-14 19:34:27 -07:00 |
|
Sebastian Ullrich
|
27c1d2f4fb
|
fix(init/meta/interactive): simp: accept local refs as simp names
|
2017-05-14 19:19:22 -07:00 |
|
Sebastian Ullrich
|
14425bd2d3
|
fix(frontends/lean/decl_util): double-elaboration of include params
|
2017-05-14 19:19:22 -07:00 |
|
Sebastian Ullrich
|
818c041922
|
fix(frontends/lean/scanner): skip_to_pos was skipping bytes instead of chars
|
2017-05-14 19:19:22 -07:00 |
|
Sebastian Ullrich
|
eb60df4409
|
fix(init/meta/interactive): case didn't find some cases
|
2017-05-14 19:19:22 -07:00 |
|
Sebastian Ullrich
|
808ab73d93
|
refactor(init): use list for expr.macro args
|
2017-05-14 19:17:28 -07:00 |
|
Sebastian Ullrich
|
42eb0c680e
|
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
|
2017-05-14 19:17:28 -07:00 |
|
Gabriel Ebner
|
85673cdd8d
|
fix(frontends/lean/definition_cmds): examples in noncomputable theories
|
2017-05-13 09:04:07 +02:00 |
|
Sebastian Ullrich
|
171a96a8de
|
refactor(library): remove all instances of `(...)
|
2017-05-12 19:13:48 +02:00 |
|
Gabriel Ebner
|
b3975c8fc1
|
chore(library/vm/vm_expr): fix compiler warning
|
2017-05-11 11:04:11 +02:00 |
|
Sebastian Ullrich
|
4b21b13649
|
refactor(init): replace has_quote class with reflected
|
2017-05-09 16:02:42 -07:00 |
|
Sebastian Ullrich
|
ead6318ee0
|
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
8c0394b294
|
refactor(library,frontends/lean): separate expr and pexpr macros
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
2825c5fbcc
|
feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
85cf1b7075
|
chore(bin/lean-gdb): pretty-print lean::optional
|
2017-05-09 16:02:41 -07:00 |
|
Sebastian Ullrich
|
aa601d3e51
|
chore(tests): move tests to correct dir
|
2017-05-09 16:02:41 -07:00 |
|
Leonardo de Moura
|
3f5bbfa0cf
|
fix(library/parray): missing lock
|
2017-05-09 13:57:28 -07:00 |
|
Leonardo de Moura
|
a3679a43a1
|
fix(library/parray): unique_lock ==> lock_guard
|
2017-05-09 13:57:28 -07:00 |
|