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

Re: Paramaterized Instantiation and Universal Quantification

A little experimentation suggests that TLC cannot perform the substitution required for parametrized instantiation in expressions involving subscripts--that is, expressions of the form [A]_v, <<A>>_v, WF_v(A), and SF_v(A).  Checking and possibly fixing this problem have been added to our (rather long) list of things to do.  Any further information that anyone can provide about when parametrized instantiation does and doesn't work would be helpful.