Menu

#36 For all statement not typechecking

open
H. Smith
Math Typing (1)
5
2012-04-12
2012-04-12
Chuck Cook
No

This doesn't type check properly in the old MathExpTypeResolver, so it would be a good test for the new type system.

Enhancement Merge_Store_Capability for Search_Store_Template;
Operation Merge (updates S: Store; clears T: Store);
requires ||S|| + ||T|| <= Max_Capacity;
ensures for all k: Key, S(k) iff #S(k) or #T(k);
end Merge_Store_Capability

Discussion


Log in to post a comment.