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

Datatype-problem



Hi there!

It's easy to extend every TYPE by an extra value as follows:

extend_it[T: TYPE]: DATATYPE
BEGIN
  new: new?
  up(down: T): up?
END extend_it

But now I want to use the extra value for the TYPE posnat:

new_theory: THEORY
BEGIN
  IMPORTING extend_it[posnat]
value: new[posnat]               % This doesn't work!
END new_theory

I think I oversee something, but I don't know what. Can somebody help me?

Thanks in advance to everyone!
Pieter Audenaert
Dept. Pure Mathematics,
University of Gent, Belgium
http://cage.rug.ac.be/~paudenae