Contents:

Library ConCert.Examples.PiggyBank.PiggyBankExtractLiquidity

From ConCert.Examples.PiggyBank Require Import PiggyBank.

(* TODO: extract the piggybank contract to Liquidity *)