Sebastian Ullrich
|
91c77680c8
|
refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean
|
2017-06-19 11:27:12 -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 |
|
Johannes Hölzl
|
1352d4a5b3
|
feat(src/frontents/lean): support for coinduction command in frontend
|
2017-06-12 20:42:48 -07:00 |
|
Johannes Hölzl
|
4d01a6548e
|
feat(library/init/meta): support mutual coinductive predicates
|
2017-06-12 20:42:48 -07:00 |
|
Johannes Hölzl
|
23f12a22a2
|
feat(library/init/meta): add command to construct coinductive predicates
|
2017-06-12 20:42:48 -07:00 |
|