I guess an example of corecursion is an inductive definition of the natural numbers: Let N be a set. 1. zero is in N. 2. If an element e is in N, then s(e) i

I guess an example of corecursion is an inductive definition of the natural numbers: Let N be a set. 1. zero is in N. 2. If an element e is in N, then s(e) is in N. You get: {zero, s(zero), s(s(zero)),...} (of course in any order, since sets are unordered). You start from zero and build the whole infinite set from that starting point. Bottom up.