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

[PVS-Help] sequence filter



 
pvs-help:
  
 I am very new to PVS.
 I want to write a function to implement the sequence filter, i.e., remove some speical symbols of that sequence. for examples:
 
   S:TYPE+
 
   a: VAR sequence[S]
 
   T: TYPE FROM S
 
   f(a) : sequence[T]   % i want the f(a) only include the symbols type of T.
 
  how to write this function f?
 
 can you help me!
  thanks in advance!
 
 
    Q.g., XU
 
   2005-9-27