Intro to total functional programming

This is a side-project to create a textbook on total functional programming in Isabelle, with an emphasis on termination analysis.