All Questions
Tagged with termination lean
2
questions
6
votes
2
answers
241
views
How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?
I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique,...
- 135
0
votes
1
answer
98
views
Well founded recursion through lists
I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with:
...
- 273