Skip to content
Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
common adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
Bib.html
Bib.v
BibTest.v
Equiv.html
Equiv.v
EquivTest.v
Hoare.html
Hoare.v
Hoare2.html
Hoare2.v
Hoare2Test.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
HoareAsLogic.html
HoareAsLogic.v
HoareAsLogicTest.v
HoareTest.v
Imp.v
ImpTest.v
LICENSE
LibTactics.html adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
LibTactics.v
LibTacticsTest.v
Makefile adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
Makefile.conf
Maps.v
MapsTest.v
MoreStlc.html
MoreStlc.v
MoreStlcTest.v
Mtac2Tactics.v
Norm.html
Norm.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
NormTest.v
PE.html
PE.v
PETest.v
Postscript.html adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
Postscript.v
PostscriptTest.v
Preface.html
Preface.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
PrefaceTest.v
README
RecordSub.html
RecordSub.v
RecordSubTest.v
Records.html
Records.v
RecordsTest.v
References.html
References.v
ReferencesTest.v
Smallstep.html
Smallstep.v
SmallstepTest.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
Stlc.html
Stlc.v
StlcProp.html
StlcProp.v
StlcPropTest.v
StlcTest.v
Sub.html
Sub.v
SubTest.v
Typechecking.html
Typechecking.v
TypecheckingTest.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
Types.html
Types.v
TypesTest.v
UseAuto.html adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
UseAuto.v
UseAutoTest.v
UseTactics.html
UseTactics.v
UseTacticsTest.v adding the Mtac2's modified version of sf/plf (only PE.v really chang… Jan 7, 2020
_CoqProject
coqindex.html
deps.gif
deps.html
deps.map
index.html
toc.html

README

#########################################################################
                           SOFTWARE FOUNDATIONS
#########################################################################

This directory contains both Coq scripts (.v files) and more readable
HTML files for the Software Foundations electronic textbook.

  - Preface.v or Preface.html
    The place to start reading, including details on how to install
    required software

  - index.html
    The book's cover page and navigation starting point

  - deps.html 
    Overview of the ordering of chapters

  - LICENSE
    Explanation of how these files may be redistributed
You can’t perform that action at this time.