This repository has been archived by the owner on Nov 17, 2020. It is now read-only.

Name		Name	Last commit message	Last commit date
parent directory ..
.gitignore		.gitignore
Bag.v		Bag.v
Correctness.v		Correctness.v
ListUtils.v		ListUtils.v
Makefile		Makefile
MonadUtils.v		MonadUtils.v
MonadicCorrectness.v		MonadicCorrectness.v
Proofs.v		Proofs.v
README.md		README.md
ReferenceFoldBag.v		ReferenceFoldBag.v
WellFormed.v		WellFormed.v
_CoqProject		_CoqProject
setup.sh		setup.sh

README.md

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