Rounding rational enclosures to posits

An enclosure determines a unique rounded value when its endpoints select the same posit code. The check uses only rational arithmetic and the format's existing appended-bit rounding rule. An inconclusive check returns none, allowing a caller to refine the enclosure.

roundPositive? is for nonnegative functions. An interval crossing zero cannot be accepted for a strictly positive target until its lower endpoint has become positive. The corresponding theorem uses monotonicity of real posit rounding.

def FloatLib.Floats.Formats.Posit.Model.Enclosure.roundPositive? (format : Format) (interval : Numerics.RationalInterval) : Option (Model format)

Accept an enclosure when both endpoints select the same nonnegative posit code.

The caller supplies the proof that its real target belongs to the enclosure in eq_roundPositive_of_roundPositive?_eq_some.