Compilers « src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	CommonSubexpressionElimination.v	11325	log plain
-rw-r--r--	CommonSubexpressionEliminationDenote.v	6289	log plain
-rw-r--r--	CommonSubexpressionEliminationInterp.v	10769	log plain
-rw-r--r--	CommonSubexpressionEliminationProperties.v	11087	log plain
-rw-r--r--	CommonSubexpressionEliminationWf.v	12734	log plain
-rw-r--r--	Conversion.v	4098	log plain
-rw-r--r--	CountLets.v	2521	log plain
-rw-r--r--	Equality.v	4226	log plain
-rw-r--r--	Eta.v	3353	log plain
-rw-r--r--	EtaInterp.v	4894	log plain
-rw-r--r--	EtaWf.v	4891	log plain
-rw-r--r--	ExprInversion.v	9589	log plain
-rw-r--r--	FilterLive.v	2861	log plain
-rw-r--r--	FoldTypes.v	1574	log plain
-rw-r--r--	Inline.v	4158	log plain
-rw-r--r--	InlineInterp.v	5718	log plain
-rw-r--r--	InlineWf.v	9560	log plain
-rw-r--r--	InputSyntax.v	11245	log plain
-rw-r--r--	InterpByIso.v	1563	log plain
-rw-r--r--	InterpByIsoProofs.v	5436	log plain
-rw-r--r--	InterpProofs.v	2609	log plain
-rw-r--r--	InterpWf.v	3036	log plain
-rw-r--r--	InterpWfRel.v	4255	log plain
-rw-r--r--	Linearize.v	4684	log plain
-rw-r--r--	LinearizeInterp.v	5253	log plain
-rw-r--r--	LinearizeWf.v	7271	log plain
-rw-r--r--	Map.v	1259	log plain
-rw-r--r--	MapCastByDeBruijn.v	3265	log plain
-rw-r--r--	MapCastByDeBruijnInterp.v	6630	log plain
-rw-r--r--	MapCastByDeBruijnWf.v	5897	log plain
-rw-r--r--	MultiSizeTest.v	7484	log plain
d---------	Named	1535	log plain
-rw-r--r--	Reify.v	23504	log plain
-rw-r--r--	Relations.v	18312	log plain
-rw-r--r--	RenameBinders.v	3071	log plain
-rw-r--r--	Rewriter.v	1541	log plain
-rw-r--r--	RewriterInterp.v	2162	log plain
-rw-r--r--	RewriterWf.v	2349	log plain
-rw-r--r--	SmartMap.v	17444	log plain
-rw-r--r--	Syntax.v	6130	log plain
-rw-r--r--	TestCase.v	11954	log plain
-rw-r--r--	Tuple.v	3245	log plain
-rw-r--r--	TypeInversion.v	7641	log plain
-rw-r--r--	TypeUtil.v	1426	log plain
-rw-r--r--	Wf.v	3298	log plain
-rw-r--r--	WfInversion.v	6959	log plain
-rw-r--r--	WfProofs.v	15872	log plain
-rw-r--r--	WfReflective.v	14089	log plain
-rw-r--r--	WfReflectiveGen.v	16987	log plain
d---------	Z	1243	log plain