All Questions
1
question
6
votes
2
answers
245
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