GitHub - robbertkrebbers/moessner: Coq formalization of moessner's theorem using coinduction

robbertkrebbers / moessner Public

Notifications You must be signed in to change notification settings
Fork 0
Star 1

Coq formalization of moessner's theorem using coinduction

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 8 Commits
site_scons/site_tools		site_scons/site_tools
.gitignore		.gitignore
LICENSE		LICENSE
README		README
SConstruct		SConstruct
moessner.v		moessner.v
moessner_1.v		moessner_1.v
moessner_2.v		moessner_2.v
prelude.v		prelude.v

Repository files navigation

PREREQUISITES
-------------

This version is known to compile with:

 - Coq 8.4pl2
 - SCons 2.0

BUILDING INSTRUCTIONS
---------------------

Say "scons" to build the full library, or "scons some_module.vo" to just 
build some_module.vo (and its dependencies).

In addition to common Make options like -j N and -k, SCons supports some 
useful options of its own, such as --debug=time, which displays the time 
spent executing individual build commands.

scons -c replaces Make clean