fact: Definition interface_to_hoare `{MayProvide ix i} `(c : contract i Ω) : ix ~> hoare Ω := fun a e => {| pre := fun ω => gen_caller_obligation c ω e ; post := fun ω x ω' => gen_callee_obligation c ω e x /\ ω' = gen_witness_update c ω e x |}.
imports: ExtLib(Functor Applicative Monad) FreeSpec.Core(Interface Impure Contract)