[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
It's easy to extend every TYPE by an extra value as follows:
extend_it[T: TYPE]: DATATYPE
up(down: T): up?
But now I want to use the extra value for the TYPE posnat:
value: new[posnat] % This doesn't work!
I think I oversee something, but I don't know what. Can somebody help me?
Thanks in advance to everyone!
Dept. Pure Mathematics,
University of Gent, Belgium