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 MHonArc.