[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: How can we extend type bool with a "bottom" element?*From*: Shtrichman Ofer <ofers@marganit.wisdom.weizmann.ac.il>*Date*: Tue, 23 Sep 1997 11:54:07 +0200 (IST)

Hi, we have a question concerning extending the predefined boolean type with an additional "bottom" element. Extending e.g. integers with a bottom element is not difficult since there exist supertypes of the integers (e.g rationals); one can just define rat_nonint: TYPE = {x: rat | FORALL (y: int): x /= y} CONTAINING 2/3 bt: rat_nonint gen_int: TYPE = {x: rat | x = bt OR integer_pred(x)}. Then bt is the designated bottom element. The most important thing in this context is that we can still use all functions which return integer values in assignments to gen_int variables. Exactly the same we would like to do with the extended boolean type that we are looking for; it is important that we can still use e.g comparison functions on integers ( which return a boolean value) in assignments to gen_bool variables. Thus we can not simply use an enumeration type. It seems that there does not exist a union type constructor in PVS so how can we define the gen_bool's? Thanks for your help Ofer and Michael =========================================================================== Ofer Shtrichman E-mail: ofers@wisdom.weizmann.ac.il http://www.wisdom.weizmann.ac.il/people/homepages/ofers/main.htm The Weizmann Institute of Science Department of Applied Mathematics & Computer Science, Rehovot 76100, Israel Tel. (W) (temporary) : (972) 08-9342856 Tel. (H) : (972) 03-5713880 ===========================================================================

- Prev by Date:
**Re: Rewrite rules don't rewrite this equality.** - Next by Date:
**Re: How can we extend type bool with a "bottom" element?** - Prev by thread:
**Re: WITH and dependent types** - Next by thread:
**Re: How can we extend type bool with a "bottom" element?** - Index(es):