GitHub - marcosfmmota/software-foundations

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 20 Commits
.depend		.depend
.gitignore		.gitignore
Auto.v		Auto.v
Basics.v		Basics.v
Bib.v		Bib.v
Equiv.v		Equiv.v
Extraction.v		Extraction.v
Hoare.v		Hoare.v
Hoare2.v		Hoare2.v
HoareAsLogic.v		HoareAsLogic.v
Imp.v		Imp.v
ImpCEvalFun.v		ImpCEvalFun.v
ImpParser.v		ImpParser.v
IndPrinciples.v		IndPrinciples.v
IndProp.v		IndProp.v
Induction.v		Induction.v
LICENSE		LICENSE
LibTactics.v		LibTactics.v
Linguagem_de_Taticas.v		Linguagem_de_Taticas.v
Lists.v		Lists.v
Logic.v		Logic.v
Makefile		Makefile
Maps.v		Maps.v
MoreStlc.v		MoreStlc.v
Norm.v		Norm.v
Objetos_de_Prova_para_Igualdade_e_Contradicao.v		Objetos_de_Prova_para_Igualdade_e_Contradicao.v
PE.v		PE.v
Poly.v		Poly.v
Postscript.v		Postscript.v
Preface.v		Preface.v
ProofObjects.v		ProofObjects.v
Proof_Objects_for_Induction.v		Proof_Objects_for_Induction.v
README		README
RecordSub.v		RecordSub.v
Records.v		Records.v
References.v		References.v
Rel.v		Rel.v
SfLib.v		SfLib.v
Smallstep.v		Smallstep.v
Stlc.v		Stlc.v
StlcProp.v		StlcProp.v
Sub.v		Sub.v
Symbols.v		Symbols.v
Tactics.v		Tactics.v
Typechecking.v		Typechecking.v
Types.v		Types.v
UseAuto.v		UseAuto.v
UseTactics.v		UseTactics.v
ap2.v		ap2.v
ap3.v		ap3.v
coqdoc.css		coqdoc.css
deps.gif		deps.gif
deps.map		deps.map
index-bg.jpg		index-bg.jpg
jquery-1.8.3.js		jquery-1.8.3.js
jquery.maphilight.min.js		jquery.maphilight.min.js
main.js		main.js
slides.js		slides.js

Repository files navigation

#########################################################################
                           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