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

Mode	Name	Size
-rw-r--r--	BoundByCast.v	2335	log plain
-rw-r--r--	BoundByCastInterp.v	7026	log plain
-rw-r--r--	BoundByCastWf.v	2181	log plain
-rw-r--r--	CommonSubexpressionElimination.v	9054	log plain
-rw-r--r--	Conversion.v	4100	log plain
-rw-r--r--	CountLets.v	2523	log plain
-rw-r--r--	Equality.v	4227	log plain
-rw-r--r--	Eta.v	3355	log plain
-rw-r--r--	EtaInterp.v	4897	log plain
-rw-r--r--	EtaWf.v	4900	log plain
-rw-r--r--	ExprInversion.v	9603	log plain
-rw-r--r--	FilterLive.v	2865	log plain
-rw-r--r--	FoldTypes.v	1577	log plain
-rw-r--r--	Inline.v	4160	log plain
-rw-r--r--	InlineCast.v	4038	log plain
-rw-r--r--	InlineCastInterp.v	6173	log plain
-rw-r--r--	InlineCastWf.v	5416	log plain
-rw-r--r--	InlineInterp.v	5738	log plain
-rw-r--r--	InlineWf.v	9567	log plain
-rw-r--r--	InputSyntax.v	11214	log plain
-rw-r--r--	InterpByIso.v	1566	log plain
-rw-r--r--	InterpByIsoProofs.v	5442	log plain
-rw-r--r--	InterpProofs.v	2613	log plain
-rw-r--r--	InterpWf.v	3039	log plain
-rw-r--r--	InterpWfRel.v	4258	log plain
-rw-r--r--	Linearize.v	2528	log plain
-rw-r--r--	LinearizeInterp.v	3445	log plain
-rw-r--r--	LinearizeWf.v	8457	log plain
-rw-r--r--	Map.v	1260	log plain
-rw-r--r--	MapCast.v	5093	log plain
-rw-r--r--	MapCastByDeBruijn.v	3226	log plain
-rw-r--r--	MapCastByDeBruijnInterp.v	6598	log plain
-rw-r--r--	MapCastByDeBruijnWf.v	5863	log plain
-rw-r--r--	MapCastInterp.v	12271	log plain
-rw-r--r--	MapCastWf.v	6576	log plain
-rw-r--r--	MultiSizeTest.v	7485	log plain
-rw-r--r--	MultiSizeTest2.v	5724	log plain
d---------	Named	1146	log plain
-rw-r--r--	Reify.v	17714	log plain
-rw-r--r--	Relations.v	18315	log plain
-rw-r--r--	RenameBinders.v	3073	log plain
-rw-r--r--	Rewriter.v	1542	log plain
-rw-r--r--	RewriterInterp.v	2164	log plain
-rw-r--r--	RewriterWf.v	2353	log plain
-rw-r--r--	SmartBound.v	6884	log plain
-rw-r--r--	SmartBoundInterp.v	8083	log plain
-rw-r--r--	SmartBoundWf.v	6326	log plain
-rw-r--r--	SmartCast.v	1630	log plain
-rw-r--r--	SmartCastInterp.v	1917	log plain
-rw-r--r--	SmartCastWf.v	3744	log plain
-rw-r--r--	SmartMap.v	17445	log plain
-rw-r--r--	Syntax.v	6097	log plain
-rw-r--r--	TestCase.v	11212	log plain
-rw-r--r--	Tuple.v	3246	log plain
-rw-r--r--	TypeInversion.v	7642	log plain
-rw-r--r--	TypeUtil.v	1427	log plain
-rw-r--r--	Wf.v	3224	log plain
-rw-r--r--	WfInversion.v	6962	log plain
-rw-r--r--	WfProofs.v	10164	log plain
-rw-r--r--	WfReflective.v	14093	log plain
-rw-r--r--	WfReflectiveGen.v	16989	log plain
d---------	Z	826	log plain