GitHub - DOFYPXY/PKU-SoftwareFoundation2022-plf: Software Foundation Course (2022 Spring) in Peking University

DOFYPXY / PKU-SoftwareFoundation2022-plf Public

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

Software Foundation Course (2022 Spring) in Peking University

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
Bib.html		Bib.html
Bib.v		Bib.v
BibTest.v		BibTest.v
Equiv.html		Equiv.html
Equiv.v		Equiv.v
EquivTest.v		EquivTest.v
Hoare.html		Hoare.html
Hoare.v		Hoare.v
Hoare2.html		Hoare2.html
Hoare2.v		Hoare2.v
Hoare2Test.v		Hoare2Test.v
HoareAsLogic.html		HoareAsLogic.html
HoareAsLogic.v		HoareAsLogic.v
HoareAsLogicTest.v		HoareAsLogicTest.v
HoareTest.v		HoareTest.v
Imp.v		Imp.v
ImpTest.v		ImpTest.v
LICENSE		LICENSE
LibTactics.html		LibTactics.html
LibTactics.v		LibTactics.v
LibTacticsTest.v		LibTacticsTest.v
Makefile		Makefile
Maps.v		Maps.v
MapsTest.v		MapsTest.v
MoreStlc.html		MoreStlc.html
MoreStlc.v		MoreStlc.v
MoreStlcTest.v		MoreStlcTest.v
Norm.html		Norm.html
Norm.v		Norm.v
NormTest.v		NormTest.v
PE.html		PE.html
PE.v		PE.v
PETest.v		PETest.v
Postscript.html		Postscript.html
Postscript.v		Postscript.v
PostscriptTest.v		PostscriptTest.v
Preface.html		Preface.html
Preface.v		Preface.v
PrefaceTest.v		PrefaceTest.v
README		README
RecordSub.html		RecordSub.html
RecordSub.v		RecordSub.v
RecordSubTest.v		RecordSubTest.v
Records.html		Records.html
Records.v		Records.v
RecordsTest.v		RecordsTest.v
References.html		References.html
References.v		References.v
ReferencesTest.v		ReferencesTest.v
Smallstep.html		Smallstep.html
Smallstep.v		Smallstep.v
SmallstepTest.v		SmallstepTest.v
Stlc.html		Stlc.html
Stlc.v		Stlc.v
StlcProp.html		StlcProp.html
StlcProp.v		StlcProp.v
StlcPropTest.v		StlcPropTest.v
StlcTest.v		StlcTest.v
Sub.html		Sub.html
Sub.v		Sub.v
SubTest.v		SubTest.v
Typechecking.html		Typechecking.html
Typechecking.v		Typechecking.v
TypecheckingTest.v		TypecheckingTest.v
Types.html		Types.html
Types.v		Types.v
TypesTest.v		TypesTest.v
UseAuto.html		UseAuto.html
UseAuto.v		UseAuto.v
UseAutoTest.v		UseAutoTest.v
UseTactics.html		UseTactics.html
UseTactics.v		UseTactics.v
UseTacticsTest.v		UseTacticsTest.v
_CoqProject		_CoqProject
coqindex.html		coqindex.html
deps.html		deps.html
deps.svg		deps.svg
index.html		index.html
toc.html		toc.html

Repository files navigation

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

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

  - 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