🚀 go-pugleaf

Donatella Castelli writes: 
| 
| In ZRM, a generic constant definition is restricted to having a value
| uniquely determined for each possible formal parameter.
| Now, I think it is sometimes useful to be able to define a generic
| object, without having to state this uniqueness condition.

The reason for this requirement is given in ZRM too (the example of the
erroneous left/right definition). 
Nevertheless: Sometimes I share your wish ;-)

| For example, I would like to define basic properties of any partial order
| among values of an as-yet-unknown type X with a generic variable
| definition
| 
|          ===[X]==========================
|          |
|          |    G  :   X <-> X
|          |
|          |----------------------
|          |
|          |    -- reflexivity --
|          |    -- antisymmetry --
|          |    -- transitivity --
|          |___________________________
| 

In this case you should define the set of all orders themselves as 
generic constants, e.g. as pre-generics:

===[X]===========================
|
|  porder _ , torder _ : P (X <-> X)
|
|---------------
|
|        -- some predicates for reflexivity and such --
|
|________________________________


For relations of whatever type you can require of them to be orders:

|  o1 : N <-> N
|  o2 : P N <-> P N
|----------------
|  torder o1
|  porder o2


| For example, if N is the set of natural numbers, I would like to
| constrain the instance G[N]  to be the usual order _<=_ , writing
| 
|       G[N]  =  (_<=_)

For particular orders of any type you have to give different, arbitrarily
chosen definitions like    o1 = (_ <= _)    and     o2 = "subset_on_N".
But how can you compare such different orders?


Regards,
	Martin

-- 
+------------------------------------------------------------------------
| Martin Carstensen, Koblenz University         cash@infko.uni-koblenz.de
|        Department of Computer Science         Voice: +49 261 9119-423
|        Rheinau 3-4, D-5400 Koblenz, Germany   Fax:   +49 261 9119-499