Leonardo de Moura
59c8a36f40
chore(library/init/meta/simp_tactic): remove unnecessary generality
2017-02-13 17:19:14 -08:00
Leonardo de Moura
c37634c815
feat(library/init): add helper functions and instances
2017-02-13 14:53:32 -08:00
Rob Lewis
46a46c9ee0
feat(norm_num): handle nat subtraction as a special case
2017-02-12 17:15:08 -08:00
Leonardo de Moura
80ac700e36
refactor(library/init): provide more general try_for, and implement tactic.try_for using it
2017-02-12 12:15:19 -08:00
Leonardo de Moura
7112f6d685
feat(library/tactic): add try_for tactic
2017-02-11 20:35:42 -08:00
Leonardo de Moura
73b1e927ff
chore(tests/lean): fix tests
2017-02-11 18:37:15 -08:00
Leonardo de Moura
41d3d42dee
feat(library/init/meta): add helper tactics
2017-02-11 18:30:38 -08:00
Leonardo de Moura
5ca18b8d2e
feat(library/init/meta): add helper functions
2017-02-11 16:52:06 -08:00
Leonardo de Moura
2f5159e7eb
feat(library/init/meta): add simple tactics for testing where a declaration was defined
2017-02-11 10:57:06 -08:00
Johannes Hölzl
9902a0d4d1
feat(src/library/tactic): apply_core returns list of all generated metavariables
2017-02-10 16:07:33 -08:00
Johannes Hölzl
bb136d63ab
feat(src/library/tactic): tactic.cases_core returns for each new goal the used constructor, a list of introduced hypotheses, and substitutions for dependent hypotheses
2017-02-10 16:07:33 -08:00
Johannes Hölzl
d7af5515d2
feat(src/library/tactic): tactic.induction_core returns for each new goal the list of introduced hypotheses and substitutions for dependent hypotheses
...
Also add to_obj(buffer<vm_obj>) to construct a vm-list of vm objects.
2017-02-10 16:07:33 -08:00
Leonardo de Moura
c0e6314f14
fix(library/init/meta,library/tactic/elaborate): bad error position when to_expr is used outside of interactive mode
2017-02-09 18:44:50 -08:00
Leonardo de Moura
c8bbb34e2a
feat(frontends/lean): add auto_param gadget
2017-02-09 15:49:10 -08:00
Leonardo de Moura
5e397795cf
fix(library/init/meta): focus tactic
...
This commit also add the interactive tactic 'focus'
2017-02-09 10:02:19 -08:00
Leonardo de Moura
3d603ec28e
feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs
2017-02-08 17:41:44 -08:00
Leonardo de Moura
32e6442d0a
feat(frontends/lean): no global universes in the frontend
2017-02-08 17:23:04 -08:00
Leonardo de Moura
c5dc8e651a
chore(library/init/meta): cleanup
2017-02-08 15:33:25 -08:00
Leonardo de Moura
54f7bf9391
fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages
...
Summary:
We minimize the number of "'sorry' used warning messages". We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"
Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.
We do not store line/col information for tactics nested in notation
declarations. Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
2017-02-07 20:25:28 -08:00
Leonardo de Moura
38557b5d6c
feat(library/init/data/nat/basic): missing lemma
2017-02-07 17:21:26 -08:00
Leonardo de Moura
e06d6aa6d4
feat(frontends/lean/elaborator): relax condition on match-convoy
2017-02-07 16:11:43 -08:00
Leonardo de Moura
96ccb148b1
feat(library/init/meta/simp_tactic): add top_down simplifier combinator
2017-02-06 20:06:13 -08:00
Leonardo de Moura
a28d6a94fd
feat(library/init/meta): add any_goals tactic
2017-02-06 16:23:29 -08:00
Leonardo de Moura
ae06844f57
chore(library/init/meta): remove unnecessarily '| failed' annotations
...
tactic and smt_tactic are instaces of monad_fail
2017-02-05 20:12:42 -08:00
Leonardo de Moura
55aa2023f4
feat(frontends/lean): add support for monad_fail type class in 'do' blocks
2017-02-05 20:09:08 -08:00
Leonardo de Moura
8b662d19ac
feat(library/init/category/monad_fail): add monad_fail type class
2017-02-05 18:46:29 -08:00
Leonardo de Moura
797b26f402
fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place
2017-02-05 18:20:10 -08:00
Leonardo de Moura
30a1876fc8
feat(library/init/meta): add add_aux_decl and abstract tactics
2017-02-05 16:00:47 -08:00
Leonardo de Moura
1eb771f5a1
chore(library/init/meta/async_tactic): missing copyright
2017-02-05 14:47:43 -08:00
Gabriel Ebner
95068e4e79
feat(library/sorry): make sorry a macro
2017-02-05 14:01:03 +01:00
Rob Lewis
d18a47b588
feat(tactic): add tactic_format instances
2017-02-04 15:30:55 -08:00
Leonardo de Moura
b28ed2453e
feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations
2017-02-04 13:44:05 -08:00
Leonardo de Moura
aff5a2dd37
fix(library/init/meta): bug introduced 9bee8ce36d
2017-02-03 17:01:46 -08:00
Leonardo de Moura
2640d3085b
fix(library/init/meta/interactive): name resolution problems in parametric sections
2017-02-03 14:04:59 -08:00
Leonardo de Moura
9bee8ce36d
fix(frontends/lean/elaborator): thunk gadget should not be considered in patterns
...
The new test demonstrates the problem.
2017-02-02 17:28:03 -08:00
Leonardo de Moura
bb9a0c79f4
feat(frontends/lean/builtin_exprs): better syntax for quoted terms with type ascription
2017-02-01 12:49:38 -08:00
Leonardo de Moura
6e7929252f
feat(frontends/lean, library/init): add 'thunk' gadget
...
We can now write
trace "hello" t
instead of
trace "hello" (fun _, t)
2017-01-31 18:41:59 -08:00
Leonardo de Moura
7cc31835e4
refactor(library/init/meta/fun_info): cleanup fun_info API
2017-01-31 18:01:54 -08:00
Leonardo de Moura
49a0d13c50
feat(library/init/coe): add coercion from A to (option A)
...
A little hack is used to make sure type class resolution will not enter
in an infinite loop.
2017-01-31 17:45:41 -08:00
Leonardo de Moura
920e845b84
refactor(library/init/meta/congr_lemma): cleanup congr_lemma API
2017-01-31 16:46:13 -08:00
Leonardo de Moura
2b56040499
fix(library/init/propext): Type => Sort
2017-01-30 19:17:57 -08:00
Leonardo de Moura
4a2ffefdaf
fix(library/init/wf): wf eliminators should be able to eliminate into Prop and Type
2017-01-30 19:14:43 -08:00
Leonardo de Moura
d3db3661af
refactor(library/init/core): simpler has_sep type class with out_param
2017-01-30 18:54:56 -08:00
Leonardo de Moura
04a8518104
refactor(library/init/core): simpler has_insert type class with out_param
2017-01-30 18:50:21 -08:00
Leonardo de Moura
f176c272b4
refactor(library/init/core): simpler has_mem type class with out_param
2017-01-30 18:43:05 -08:00
Leonardo de Moura
5da8b205b9
feat(library/type_context, frontends/lean/elaborator): type classes with output parameters
2017-01-30 18:32:54 -08:00
Leonardo de Moura
d34386fef7
perf(frontends/lean/tactic_notation): closes #1345
...
We can now elaborate
https://gist.github.com/gebner/439273deee592603190d4f8b4447295b
in 1.6 secs and using less than 500Kb of stack space.
It was takins 44 secs and 5Mb before this commit.
Two modifications:
1) Use pre_monad.seq instead of pre_monad.and_then.
They have the same implementation, but seq is not marked as [inline].
2) Modify how we concatenate the tactics in a begin...end block.
Before: (((a_1 ++ a_2) ++ a_3) ++ a_4)
After: ((a_1 ++ a_2) ++ (a_3 ++ a_4))
2017-01-30 14:13:53 -08:00
Leonardo de Moura
41bf46dbba
chore(library/init): adjust Sort vs Type in definitions
2017-01-30 12:50:18 -08:00
Leonardo de Moura
3b38f71f11
fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type
...
We had to change subtype to use Sort since the axiom
strong_indefinite_description uses it.
see #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
a6f26f0b74
chore(library): poly_unit ==> punit
...
psum, pprod and punit are used internally.
see #1341
2017-01-30 11:54:00 -08:00
