Leonardo de Moura
61254847fb
fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression)
2017-02-20 14:51:59 -08:00
Leonardo de Moura
ddee94b831
fix(frontends/lean/elaborator): incorrect invariant due to error recovery
...
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
2017-02-20 14:30:10 -08:00
Leonardo de Moura
f5cbdff893
feat(library/tools/mini_crush/default): provide equational lemmas for "relevant" functions to rsimp; make sure we do not get stuck in ematching loop by using try_for
2017-02-19 20:56:13 -08:00
Leonardo de Moura
f140095d7b
feat(library/tools/mini_crush/default): improve mini_crush
2017-02-19 20:26:30 -08:00
Leonardo de Moura
1ca5c78cf8
feat(library/tools/mini_crush): improve mini_crush
2017-02-19 18:33:12 -08:00
Leonardo de Moura
a41aac0e6a
feat(library/tools/mini_crush): add tracing messages, and more examples
2017-02-19 17:27:09 -08:00
Leonardo de Moura
0fb5a01f17
feat(library/tools): add mini_crush
2017-02-19 16:21:12 -08:00
Leonardo de Moura
ec6e1e389b
chore(tests/lean/run/cpdt): simplify
2017-02-19 13:49:19 -08:00
Leonardo de Moura
50f4a28fc3
feat(library/init/meta/smt/interactive): rsimp for smt_tactic
2017-02-19 13:31:03 -08:00
Leonardo de Moura
296d4b0f09
refactor(library/tactic, library/init/meta): simplify_config => simp_config
2017-02-19 13:10:36 -08:00
Leonardo de Moura
b52e8d67be
feat(library/init/meta): simp&intro tactics
2017-02-19 13:02:27 -08:00
Leonardo de Moura
d20319693d
feat(library/init/meta): cleanup interface using default parameters
2017-02-19 12:12:34 -08:00
Leonardo de Moura
0d22410e2e
feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode
2017-02-19 12:11:22 -08:00
Leonardo de Moura
2928273a1e
feat(tmp/mini_crush): add experiments
2017-02-18 22:52:50 -08:00
Leonardo de Moura
203a0ac932
feat(library/tactic/smt/smt_state): more restrictive default intros
2017-02-18 22:48:34 -08:00
Leonardo de Moura
505efb642a
feat(library/init/meta/rb_map): add missing function
2017-02-18 22:44:16 -08:00
Leonardo de Moura
0a99910c52
feat(library/init/meta): add exception set to rsimp attributes, use iff lemmas
2017-02-18 19:43:21 -08:00
Leonardo de Moura
0626835530
feat(library/init/meta): add native name_set
2017-02-18 19:07:50 -08:00
Leonardo de Moura
bed3e6c2fd
feat(library/tactic/smt): add get_config and use it to implement slift
...
smt_tactic.slift was losing the configuration.
2017-02-18 17:52:45 -08:00
Leonardo de Moura
2f6f1eb458
feat(library/init): add helper functions
2017-02-18 16:23:15 -08:00
Leonardo de Moura
b1acaf50ee
feat(library/init/meta/rb_map): add rb_set and helper functions
2017-02-18 16:22:15 -08:00
Leonardo de Moura
c065faaf1f
feat(frontends/lean/elaborator): improve ^. notation
2017-02-18 16:20:21 -08:00
Leonardo de Moura
74f7bc0473
feat(frontends/lean): improve notation for converting infix notation into functions
2017-02-17 23:11:22 -08:00
Leonardo de Moura
077176b82f
feat(frontends/lean): add Haskell-like for converting infix notation into functions
...
Examples:
qsort (<) [20, 5, 10, 3, 2, 14, 1]
foldl (+) 0 [1, 2, 3]
2017-02-17 22:51:50 -08:00
Leonardo de Moura
10c881266b
refactor(frontends/lean): add parse_lparen
2017-02-17 21:46:39 -08:00
diakopter
554e6bad90
chore(library): fix warning
2017-02-17 21:09:23 -08:00
Leonardo de Moura
4f3fd2cba6
feat(library/init/data/list/qsort): add temp qsort as meta definition
2017-02-17 21:07:09 -08:00
Leonardo de Moura
7eef501ae1
chore(*): remove mpfr dependency
...
closes #1380
2017-02-17 20:36:53 -08:00
Johannes Hölzl
bb4920fcbc
feat(library/vm/vm_expr): export instantiate_univ_params
2017-02-17 20:08:18 -08:00
Johannes Hölzl
3db0ebdcf0
feat(library/tactic/match_tactic): return also assignments for universe meta-variables
2017-02-17 20:08:09 -08:00
diakopter
19606fd197
chore(util,kernel,library): clang warnings
2017-02-17 20:01:34 -08:00
Sebastian Ullrich
b9424975b3
refactor(init/meta): replace dynamically-checked quotes where possible
2017-02-17 19:59:57 -08:00
Gabriel Ebner
0c2878e509
fix(frontends/lean/definition_cmds): copy position for equation in meta definitions
...
Fixes #1377 .
2017-02-17 19:57:49 -08:00
Leonardo de Moura
a36e20f0cd
feat(tmp/mini_crush): update
2017-02-17 19:56:14 -08:00
Leonardo de Moura
98b2eb893d
chore(tests/lean/run): fix tests
2017-02-17 19:55:49 -08:00
Leonardo de Moura
a9122a2c0a
chore(library/init/meta): use general when
2017-02-17 19:51:40 -08:00
Leonardo de Moura
632c98aade
feat(library/data/list): cleanup proofs
2017-02-17 19:42:57 -08:00
Leonardo de Moura
a4f43d36a6
feat(library/init/meta/smt): add rsimp
2017-02-17 19:40:38 -08:00
Leonardo de Moura
c51d9ad4f4
feat(library/init/meta): add simph: a shorter simp_using_hs
2017-02-17 13:45:03 -08:00
Leonardo de Moura
03d53b82bd
feat(library/init/meta/contradiction_tactic): minor improvement
2017-02-17 13:44:42 -08:00
Leonardo de Moura
d3c340a30c
feat(library/init/meta): improve induction tactic interface
...
It uses .rec recursor when it is not specified
2017-02-17 10:58:51 -08:00
Leonardo de Moura
e16c3a0bee
feat(library/init/meta/fun_info): add fold_explicit_args
2017-02-17 10:21:06 -08:00
Sebastian Ullrich
d402b2a467
feat(frontends/lean/print_cmd): add to info_manager when not overloaded
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
84f3e2a492
refacotr(init/meta/interactive): clean up parameter gadgets
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
69ed7b940f
refactor(init/meta/interactive): query position information dynamically
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
4d41b03168
chore(frontends/lean,library/tactic): remove old tactic_state functions
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
6b611eb030
chore(.travis.yml): fail eagerly
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
e8fa54cc51
refactor(init/meta): move macro creation defs from expr to pexpr
2017-02-17 13:45:57 +01:00
Sebastian Ullrich
9d8c84713c
refactor(*): reduce exception context info from expr to pos_info
2017-02-17 13:45:57 +01:00
Sebastian Ullrich
e14eab2db8
chore(test/lean/interactive): do not test for exact source information
2017-02-17 13:45:56 +01:00
