From: Laurent V. <lau...@sy...> - 2009-06-17 13:16:42
|
Hi, Le 17 juin 09 à 15:04, Paulo J. Matos a écrit : > In the wiki page: > http://wiki.event-b.org/index.php/ASCII_Representations_of_the_Mathematical_Symbols_(Rodin_User_Manual) > > There is a reference in the bottom to: oftype > It's the first time I hear about this character. What's its usage for > in Event-B? it is used to specify a type for empty sets or bound identifiers. For instance, if you type in a formula: ({} oftype POW(S)) it denotes the empty set of type POW(S). Similarly, you could type: !(a oftype INT). true to write a typed universally quantified predicate. It is not expected that users need to use this operator when entering models. However, when proving it can become very handy (e.g., for instantianting a universal or existential quantifier). Laurent. |