Mario Carneiro
c06c62c03e
refactor(init/data/nat/gcd): define gcd using eqn compiler
2017-06-27 18:55:52 -07:00
Mario Carneiro
9f2980a524
feat(init/data/int): int lemmas, more bitwise theorems
2017-06-27 18:55:52 -07:00
Mario Carneiro
9f4f93e931
feat(init/data/int): prove int bitwise ops
2017-06-27 18:55:52 -07:00
Mario Carneiro
e705d89490
feat(init/data/int): bitwise ops for integers
2017-06-27 18:55:52 -07:00
Mario Carneiro
a63bafcc5c
refactor(init/data/nat/bitwise): change definitions to avoid WF
...
The type-correctness of binary_rec_eq (the statement, not the proof) depends on unfolding the embedded well-founded definition of mod. This definition avoids it by using two simpler functions bodd and div2 that reduce well in the kernel.
2017-06-27 18:55:52 -07:00
Sebastian Ullrich
9033cba7d3
feat(frontends/lean,init/meta/interactive): assume and suppose tactics
2017-06-27 18:50:10 -07:00
Leonardo de Moura
6ba425da6a
feat(library/init/meta/interactive): add apply_with interactive tactic
...
The new tactic allows us to set apply_cfg in interactive mode.
2017-06-27 18:37:13 -07:00
Leonardo de Moura
e971acabb0
feat(library/init/meta): handle auto_params and opt_params at apply tactic
2017-06-27 18:17:48 -07:00
Leonardo de Moura
cdec07fc81
feat(library/init/meta/interactive): address issue raised in comment at #1374
...
The example at
https://github.com/leanprover/lean/issues/1342#issuecomment-307912291
2017-06-27 16:45:21 -07:00
Leonardo de Moura
9b03309d83
fix(library/equations_compiler): performance problem reported by @dselsam
2017-06-27 15:24:12 -07:00
Leonardo de Moura
9fdb1c4a4d
chore(library/init/meta/tactic): mark id_locked as [inline]
2017-06-27 13:43:24 -07:00
Leonardo de Moura
5a2b7348f9
feat(library/tactic/apply_tactic): make apply tactic more robust
...
See issue #1342
Support for auto_param and opt_param have not been implemented yet.
2017-06-27 10:42:26 -07:00
Mario Carneiro
b9c2659b5d
fix(init/meta/interactive): generalize2 rollback if typecheck fails
2017-06-26 12:35:27 -07:00
Daniel Selsam
d95b003c0b
feat(init/meta/congr_tactic.lean): tactic to apply congruence rules
2017-06-26 09:17:53 -04:00
Leonardo de Moura
ce5ca79edf
feat(library/init/meta): add type_check tactic
...
closes #1697
2017-06-25 15:26:32 -07:00
Mario Carneiro
d3d5982544
fix(init/meta/mk_dec_eq_instance): bug for dependent structures
2017-06-25 14:55:47 -07:00
Gabriel Ebner
30a9217a78
feat(library/type_context): unfold lemmas in major premise of acc.rec
2017-06-22 08:33:11 -07:00
Sebastian Ullrich
4d5d2abcba
fix(init/meta): fix build
2017-06-22 08:24:36 -07:00
Sebastian Ullrich
0a48809469
refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let
2017-06-22 08:03:23 -07:00
Mario Carneiro
9f31096892
refactor(init/meta/interactive): rename pose -> define
2017-06-22 08:03:23 -07:00
Mario Carneiro
b775a01fba
refactor(init/meta/interactive): merge assert -> note
2017-06-22 08:03:23 -07:00
Leonardo de Moura
671b6240c1
fix(library/init/meta): make sure rw still produces useful error messages
2017-06-21 20:58:59 -07:00
Leonardo de Moura
14d768ffa2
feat(library/init/meta/interactive): add simp_all tactic
...
@Armael I added the simp_all tactic. See new test for an example.
2017-06-21 20:43:56 -07:00
Leonardo de Moura
058d073cba
feat(library/init/meta/interactive): allow user to write rw [f] to rewrite using the equational lemmas for f
...
The tactic succeeds if the expression can be rewritten using one of the
equational lemmas associated with `f`.
See discussion at #1680
2017-06-21 18:56:18 -07:00
Leonardo de Moura
35b99aafb2
feat(library/init/category/combinators): add list.mfirst
2017-06-21 18:53:22 -07:00
Leonardo de Moura
b9dee04fdb
feat(library/tactic/simplify): add single_pass simplifier option (default is false)
2017-06-21 16:41:54 -07:00
Scott Morrison
629d5ebbe8
feat(init/meta/simp_tactic) tactics that revert hypotheses should allow elet expressions
...
Conflicts:
library/init/meta/simp_tactic.lean
2017-06-21 13:58:46 -07:00
Scott Morrison
6aba80d389
feat(library/init/meta/simp_tactic,library/init/meta/interactive) interactive tactics for unfold_projection
2017-06-21 13:51:52 -07:00
Mario Carneiro
636e65a216
fix(init/meta/interactive): elab terms of change-with using same type
2017-06-20 12:34:29 -07:00
Leonardo de Moura
cfa34dc83e
chore(library): remove workarounds for issue #1682
2017-06-19 16:09:12 -07:00
Sebastian Ullrich
91c77680c8
refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
4d444b8b18
feat(init/meta/lean/parser): persist environment in tactic_to_parser
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
492cb20438
feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env
2017-06-19 11:27:12 -07:00
Gabriel Ebner
2e142d87ae
fix(library/init/data/repr): give correct implementation of nat.repr
2017-06-19 16:20:27 +02:00
Gabriel Ebner
82bb37422d
fix(library/init/data/int): add to_string instance for integers
2017-06-19 14:30:58 +02:00
Leonardo de Moura
b8fa7f5311
fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean
...
See #1664
2017-06-18 18:33:27 -07:00
Leonardo de Moura
049fecee23
fix(library/init): name has_repr instance is actually a has_to_string instance
...
See #1664
2017-06-18 18:33:16 -07:00
Leonardo de Moura
8b88f21c91
refactor(library): add has_to_string back (but it produces unquoted values)
...
See issue #1664
2017-06-18 18:30:10 -07:00
Leonardo de Moura
dc1a1c8540
refactor(library): has_to_string ==> has_repr
...
See issue #1664
This is just the first step to implement proposal described at issue #1664 .
2017-06-18 18:29:19 -07:00
Leonardo de Moura
7528e14e68
feat(frontends/lean,shell/server): "hole" command
2017-06-14 21:56:17 -07:00
Leonardo de Moura
55c8627f2c
feat(frontends/lean): {! ... !} takes a list of pre-terms
2017-06-13 22:19:17 -07:00
Leonardo de Moura
dac6eec556
feat(library/tactic): add hole_command bookkeeping
2017-06-13 21:12:29 -07:00
Johannes Hölzl
89136339ff
fix(library/init/meta): error message mentions now solve1 instead of focus
2017-06-12 20:42:48 -07:00
Johannes Hölzl
8d438e1012
feat(library/init/meta): add coinduction method
2017-06-12 20:42:48 -07:00
Johannes Hölzl
4368e6b774
fix(library/init/meta): proofs for coinductive predicates introduce now local variable
2017-06-12 20:42:48 -07:00
Johannes Hölzl
b46532bd39
feat(library/init/meta): add error messages when constructing coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
652cbee425
feat(library/init/meta): support nesting for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
3e6c7efd48
feat(library/init/meta): corec_on for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
e4d8efc91b
feat(library/init/meta): add attributes and mark parameters and locals as implicit in theorems proveded for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
f19e1742dd
feat(library/init/meta): produce cases_on for coinductive predicates
2017-06-12 20:42:48 -07:00
