Code for the "Total Functions for Automated Reasoning" talk at LambdaWorld'25 Slides: slides.pdf Mostly based on Harrison, [2009] "Handbook of Practical Logic and Automated Reasoning" Requires the cubical-mini, agdarsec-cm and prettyng-cm libraries.