Leonardo de Moura
|
e61d0be561
|
feat: isolate fixed prefix at well-founded recursion
closes #1017
|
2022-02-18 10:40:32 -08:00 |
|
Leonardo de Moura
|
9ee529e5ce
|
fix: use PSum instead of Sum when using well-founded recursion
See new test for example that did not work with `Sum` because type
alpha was `Sort u`.
|
2022-02-17 16:14:34 -08:00 |
|
Leonardo de Moura
|
45bd328d5e
|
fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic
|
2022-01-12 08:28:03 -08:00 |
|
Leonardo de Moura
|
381f66428a
|
chore: use termination_by'
We are going to define a higher level syntax for `termination_by`.
|
2022-01-11 15:00:53 -08:00 |
|
Leonardo de Moura
|
4c918a2363
|
feat: use default_decreasing_tactic at WF/Fix.lean
|
2022-01-10 14:55:38 -08:00 |
|
Leonardo de Moura
|
790a22c5df
|
test: mutual recursion by well-founded recursion
|
2021-10-06 16:38:42 -07:00 |
|