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

Re: type vs. set

Hanne,

>   R((f:[T -> real]), (c:T), 
>     (d: {x:T | compact_interval_subset?(c,x,fullset[T])} )) 
>   : [(closed_interval(c,d)) -> real] 
>   = LAMBDA (u : (closed_interval(c,d))) : f(u)
> 
> Now, can I actually prove this TCC, or can I change my definition of 
> R to something equivalent which will work?

in your definition of R in theory test, use T_pred instead of
fullset[T]:

  R(f:[T->real],c:T,d:{x:T | compact_interval_subset?(c,x,T_pred)}) 
    : [(closed_interval(c,d)) -> real]
  = LAMBDA (u : (closed_interval(c,d))) : f(u)

Then, M-x tcp will do.

Regards,

	- Holger

-- 
----------------------------------------------------------------------
Holger Pfeifer                              Tel.: (+49) 731 / 502-4124
Universitaet Ulm                             Fax: (+49) 731 / 502-4119
Abt. Kuenstliche Intelligenz          pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm          
http://www.informatik.uni-ulm.de/ki/pfeifer.html   
----------------------------------------------------------------------