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

problem in pvs



Hi!

We are working with PVS at the University of Gent, Belgium. Can you help
us with the following problem: We want to extend the set of integers in
pvs with 1 extra symbol, creating a superset. We have to do this in the
following context: suppose you have a function f [int->int], but somewhere
in the domain we want to map f to the new symbol, call it 'a'.
This value doensn't need to have integer-properties. All we need is a set
which contains all integers, and an extra value a. Everything I tried
didn't work. Any suggestions? Thanks in advance.
				
			Best regards,
			Pieter Audenaert
			University of Gent, Belgium
			Department of Pure Mathematics and ComputerAlgebra