Closed cyrus- closed 2 months ago
we insert fixpoints automatically in elaboration, but for pedagogical purposes it would be useful to also write them explicitly
we insert fixpoints automatically in elaboration, but for pedagogical purposes it would be useful to also write them explicitly