Name	Name	Last commit message	Last commit date
Latest commit History 164 Commits
euler-dafny	euler-dafny
.gitignore	.gitignore
2dMetric.dfy	2dMetric.dfy
AVL.dfy	AVL.dfy
Abstraction.dfy	Abstraction.dfy
Ackermann.dfy	Ackermann.dfy
Ackermann.smt2	Ackermann.smt2
Allocate.dfy	Allocate.dfy
ArithmeticCompiler.dfy	ArithmeticCompiler.dfy
Array2dAs1d.dfy	Array2dAs1d.dfy
ArrayExamples.dfy	ArrayExamples.dfy
ArrayMap.dfy	ArrayMap.dfy
Assert.dfy	Assert.dfy
AutomataParsing.v	AutomataParsing.v
BST.dfy	BST.dfy
BijectiveMap.dfy	BijectiveMap.dfy
BinaryTreeSerializer.v	BinaryTreeSerializer.v
BoogieDatatypes.bpl	BoogieDatatypes.bpl
BottomUpCheerios.v	BottomUpCheerios.v
Braun.dfy	Braun.dfy
CancellativeSemigroups.v	CancellativeSemigroups.v
ClassesVersusTraits.dfy	ClassesVersusTraits.dfy
ConcurrentImp.v	ConcurrentImp.v
ConstructorExport.dfy	ConstructorExport.dfy
DAG.dfy	DAG.dfy
DafnyAst.hs	DafnyAst.hs
DiffLists.v	DiffLists.v
EarlyExitAutomata.v	EarlyExitAutomata.v
EnumerateLists.py	EnumerateLists.py
EnumeratePatches.py	EnumeratePatches.py
EnumeratePatches.v	EnumeratePatches.v
EvenPredicate.dfy	EvenPredicate.dfy
ExtensionalMaps.v	ExtensionalMaps.v
FiniteInjectionSurjection.v	FiniteInjectionSurjection.v
FloydTortoiseHare.dfy	FloydTortoiseHare.dfy
FloydTortoiseHare2.dfy	FloydTortoiseHare2.dfy
FrontierTree.dfy	FrontierTree.dfy
FunctorExample.v	FunctorExample.v
GADTGraph.ml	GADTGraph.ml
GaussianElim.ml	GaussianElim.ml
GenericMax.dfy	GenericMax.dfy
Goddity.hs	Goddity.hs
HeapRecursion.dfy	HeapRecursion.dfy
HigherOrder.dfy	HigherOrder.dfy
Hyper.dfy	Hyper.dfy
ImperativeCheerios.v	ImperativeCheerios.v
IndependentComposition.v	IndependentComposition.v
InductionLoop.dfy	InductionLoop.dfy
InductionPrinciples.v	InductionPrinciples.v
InfiniteHats.dfy	InfiniteHats.dfy
InfiniteValleys.v	InfiniteValleys.v
InsertionSort.dfy	InsertionSort.dfy
Iterators.dfy	Iterators.dfy
IteratorsAsCoroutines.dfy	IteratorsAsCoroutines.dfy
LetExpressionTriggers.dfy	LetExpressionTriggers.dfy
Linear.dfy	Linear.dfy
LinearAlgebra.smt2	LinearAlgebra.smt2
Links.dfy	Links.dfy
ListInductionWithPrefix.v	ListInductionWithPrefix.v
Makefile	Makefile
MapBuildValuesFalse.dfy	MapBuildValuesFalse.dfy
MatrixMultiplication.dfy	MatrixMultiplication.dfy
Merkel.dfy	Merkel.dfy
MetricSpace.dfy	MetricSpace.dfy
Modules.dfy	Modules.dfy
MutualRecursion.dfy	MutualRecursion.dfy
NativeIntExponential.dfy	NativeIntExponential.dfy
NetworkExample.dfy	NetworkExample.dfy
NotLockStep.dfy	NotLockStep.dfy
OneHundredPrisonersAndALightbulb.dfy	OneHundredPrisonersAndALightbulb.dfy
Parser.dfy	Parser.dfy
PatternMatchingLet.dfy	PatternMatchingLet.dfy
Paxos.v	Paxos.v
Percentile.dfy	Percentile.dfy
Peterson.bpl	Peterson.bpl
PointedEarlyExitAutomata.v	PointedEarlyExitAutomata.v
PreludeModel.dfy	PreludeModel.dfy
ProducerConsumerMath.dfy	ProducerConsumerMath.dfy
README.md	README.md
Reduction.v	Reduction.v
Reduction2.v	Reduction2.v
Refinement.dfy	Refinement.dfy
RegexLemma.v	RegexLemma.v
RegexSF.v	RegexSF.v
Regular.dfy	Regular.dfy
RegularGrammars.v	RegularGrammars.v
ReverseInPlace.dfy	ReverseInPlace.dfy
ReverseString.dfy	ReverseString.dfy
RoseTree.dfy	RoseTree.dfy
Simulation.dfy	Simulation.dfy
SquareRoot.dfy	SquareRoot.dfy
StreamlessSets.v	StreamlessSets.v
SubsetTypes.dfy	SubsetTypes.dfy
SumArray.dfy	SumArray.dfy
TAPL.dfy	TAPL.dfy
Table.v	Table.v
TableNoDep.v	TableNoDep.v
Ticket.dfy	Ticket.dfy
TotalOrder.v	TotalOrder.v
Tutorial.fst	Tutorial.fst

Name

Last commit message

Last commit date

164 Commits