UNA

Allow UNA's in type declaration OR in the theory

ex. vocabulary V:{ type person = UNA{P1;P2; P3} }

or

vocabulary V:{ type person } theory T: V{ person = UNA{...} }

Although it seems that this way, we are mixing our structure and vocabulary (or mixing theory and structure) this is not always the case

sometimes, parts of the structure are inherent to the theory such as Dir = {Hor, Ver} in battleship

This is really needed in the theory

Comments (3)