Module Wp

module Wp: sig .. end
Weakest preconditions.


No function is directly exported: they are registered in Db.Properties.