A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory

Peter Dybjer. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic, 65(2):525-549, 2000.

Abstract

Abstract is missing.