Controlling unfolding in type theory

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2

We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…