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

question on dependent typing



Hi,
The following spec gives what appears to be an unprovable TCC:

t1  : THEORY

  BEGIN

  a_type  : type = [#
                  b : setof[int],
                  c : setof[(b)]
               #]

d   : var int
t   : var a_type


add(d,t) : a_type = t with [b := add(d, t`b)]

END t1

... and yields:

% Subtype TCC generated (at line 16, column 20) for  c(t)
  % unfinished
add_TCC1: OBLIGATION
  FORALL (d, t): FORALL (x: int): t`b(x) IFF add[int](d, t`b)(x);

I'm unsure why I'm getting this.   Can anyone shed some insight?

Thanks very much in advance,
Kurt