Re: Real midpoints

My point is that the definition of g is neither recursive nor co-recursive. The definition of g is merely expressed as a fixpoint equation, and Peter has set up things so that there is indeed a unique solution to this equation. However, the reason the fixpoint is unique is because the "h" part is contracting, and not because the equation is co-recursive.

what exactly do you mean by corecursive? (it's guarded, and guarded equations do have unique fixpoints.) -- dusko