Re: [isabelle] Interval Type
In the paper, there is no need for infinite bounds, so i guess all the
alternatives are ok. If you want to include infinite bounds, you
definitely need more, e.g. types interval = (real option) * (real option).
It also depends on what you want to prove for the intervals. If you want
to prove e.g. that the intervals form a semi-lattice, then maybe the types
approach is more suitable.
I have no experience with records, may be an other one could comment on
Hope it helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and