Skip to content

Latest commit

 

History

History

bag

GHC's Bag module

This directory contains the translated version of GHC's Bag.hs file in Bag.v, and proofs about it in Proofs.v. The translated file is static.

First, you will need to have built the base library, in ../ghc-base; see the README there for more information.

To compile these proofs, run make