Proving Termination in Lean 4, pt. 1
You are filled with determination… Doing proofs from the book Programming Language Foundations in Agda in the Lean 4 prover has really been a refreshing experience for me. However, things did get annoying sometimes for me, especially when I just couldn’t get pass the termination check. Although I haven’t seen every piece of the puzzle yet, I do hope that by sharing what I have seen so far, this blog post could save you some time from bashing “lean termination” into your search box , which could potentially lead you to some random web pages about Lean Manufacturing....