Leonardo de Moura
156e5603d6
feat(library/init/category/combinators): put list combinators in the namespace list
...
In this way we can use them with the ^. notation
2017-03-05 21:30:30 -08:00
Leonardo de Moura
59c0cbd2e4
chore(library): test new '^.' notation in the standard library, and cleanup definitions using it
2017-03-05 21:21:50 -08:00
Leonardo de Moura
1cdf13821c
feat(library/init/data/unsigned): add basic unsigned operations
2017-03-05 16:14:16 -08:00
Sebastian Ullrich
ddfdca2e57
chore(init/meta): replace some uses of to_expr `(...) with ``(...)
2017-03-05 08:37:16 -08:00
Sebastian Ullrich
5d68938a9c
feat(frontends/lean): expr literals ```(...)
2017-03-05 08:37:16 -08:00
Leonardo de Moura
525242561a
fix(library/init/meta/tactic): use zeta reduction by default in the abstract tactic
...
Abstracting let-exprs may produce type errors.
In the future we may consider another strategy for `abstract`.
First, we try to abstract the `let`, then if it fails, we expand.
Not sure if this is a good idea.
2017-03-02 11:34:28 -08:00
Leonardo de Moura
b1848efbc4
chore(library/init/meta): add head prefix to head reduction tactics, and add zeta tactic (that applies zeta reduction to all subterms)
2017-03-02 10:55:38 -08:00
Leonardo de Moura
2fb5f6a49e
feat(library/init/meta): add subst_vars tactic
2017-03-01 15:11:17 -08:00
Leonardo de Moura
04e27eb96f
feat(library/init/meta/tactic): add applyc tactic
2017-02-25 12:55:28 -08:00
Leonardo de Moura
7ec0505e94
chore(library/init/meta/vm): style
2017-02-25 12:47:58 -08:00
Leonardo de Moura
35acad642c
feat(library/init/meta/tactic): add to_string instance
2017-02-25 12:47:46 -08:00
Leonardo de Moura
57c125c60e
chore(library/init/meta/expr): unsigned ==> nat
2017-02-24 19:34:11 -08:00
Leonardo de Moura
921d72b6c4
feat(library/init/meta): add helper tactics
2017-02-24 16:26:47 -08:00
Gabriel Ebner
79afaa7421
feat(library/init/meta/tactic): add timetac combinator
2017-02-24 20:17:19 +01:00
Leonardo de Moura
552a185e6a
feat(frontends/lean): 'let' in 'do' blocks
2017-02-24 09:10:36 -08:00
Leonardo de Moura
5c7ade4ee4
chore(library/init/meta/vm): indentation
2017-02-23 09:32:20 -08:00
Jared Roesch
9b80e3bb62
feat(library/init/meta/vm): add decidable_eq for vm_obj_kind
2017-02-23 09:31:57 -08:00
Sebastian Ullrich
8c50efeb75
refactor(init/meta/lean/parser): simplify sep_by
2017-02-23 01:52:14 +01:00
Sebastian Ullrich
a443a5b7a6
chore(init/meta,tools/super): remove obsolete set_option eqn_compiler.max_steps
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3
feat(frontends/lean/parser): expr patterns
2017-02-23 01:52:13 +01:00
Leonardo de Moura
7e6a10bd1b
chore(tests/lean): fix tests, and environment.decl_pos
2017-02-21 11:21:02 -08:00
Sebastian Ullrich
69741061b0
refactor(init/meta): drop obsolete X.to_expr functions
2017-02-21 11:06:39 -08:00
Sebastian Ullrich
a053175714
refactor(init/meta,library/vm): use structure for position information
2017-02-21 11:06:39 -08:00
Leonardo de Moura
d1d5428808
feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes
2017-02-21 10:45:31 -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
0fb5a01f17
feat(library/tools): add mini_crush
2017-02-19 16:21:12 -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
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
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
Sebastian Ullrich
b9424975b3
refactor(init/meta): replace dynamically-checked quotes where possible
2017-02-17 19:59:57 -08:00
Leonardo de Moura
a9122a2c0a
chore(library/init/meta): use general when
2017-02-17 19:51:40 -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
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
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
