[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