🚀 go-pugleaf

In <1992Jul24.124820.28528@ctr.columbia.edu> castelli@iei.pi.cnr.it (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.
>We could call this object a "generic variable" and any standard generic
>constant could be considered a particular instance of a generic variable.

>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

  ... 39 lines deleted ...

What about defining as a generic constant the set of *all* partial
orders on X?  Then you can introduce as a constant some particular
partial order drawn from this set.  eg to introduce a new partial
ordering on the naturals you can write

  G: PartialOrder[Nat]

You can then further constrain G as you wish, perhaps by

  G = (_ <= _)

Would this construct do for your "generic variable"?

Andy Gravell