Open dtwelch opened 8 years ago
for instance: Operation Rem_Capacity(preserves S : Stack) : Integer; ens Rem_Capacity = ... MathVarLikeReferences should be able to complete Rem_Capacity in this instance (when typing the ensures clause).
MathVarLikeReference
Rem_Capacity
for instance: Operation Rem_Capacity(preserves S : Stack) : Integer; ens Rem_Capacity = ...
MathVarLikeReference
s should be able to completeRem_Capacity
in this instance (when typing the ensures clause).