Coco: Corecursion with Compositional Heterogeneous Productivity

Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur

Contemporary proof assistants impose restrictive syntactic guardedness conditions that reject many valid corecursive definitions. Existing approaches to overcome these restrictions…