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

Mode	Name	Size
-rw-r--r--	Application.v	8136	log plain
-rw-r--r--	ApplicationLemmas.v	4018	log plain
-rw-r--r--	ApplicationRelations.v	1626	log plain
-rw-r--r--	BoundByCast.v	12609	log plain
-rw-r--r--	CommonSubexpressionElimination.v	9095	log plain
-rw-r--r--	Conversion.v	4034	log plain
-rw-r--r--	CountLets.v	2452	log plain
-rw-r--r--	Equality.v	9313	log plain
-rw-r--r--	ExprInversion.v	10982	log plain
-rw-r--r--	FilterLive.v	2942	log plain
-rw-r--r--	Inline.v	4241	log plain
-rw-r--r--	InlineInterp.v	6500	log plain
-rw-r--r--	InlineWf.v	4085	log plain
-rw-r--r--	InputSyntax.v	7139	log plain
-rw-r--r--	InterpProofs.v	2400	log plain
-rw-r--r--	InterpWf.v	3370	log plain
-rw-r--r--	InterpWfRel.v	4635	log plain
-rw-r--r--	Linearize.v	2562	log plain
-rw-r--r--	LinearizeInterp.v	3375	log plain
-rw-r--r--	LinearizeWf.v	8410	log plain
-rw-r--r--	Map.v	1260	log plain
-rw-r--r--	MapCast.v	5537	log plain
-rw-r--r--	MultiSizeTest.v	7485	log plain
-rw-r--r--	MultiSizeTest2.v	5527	log plain
d---------	Named	290	log plain
-rw-r--r--	Reify.v	15475	log plain
-rw-r--r--	Relations.v	16181	log plain
-rw-r--r--	SmartMap.v	13822	log plain
-rw-r--r--	Syntax.v	6058	log plain
-rw-r--r--	TestCase.v	10022	log plain
-rw-r--r--	Tuple.v	3202	log plain
-rw-r--r--	TypeInversion.v	4336	log plain
-rw-r--r--	Wf.v	3321	log plain
-rw-r--r--	WfInversion.v	5479	log plain
-rw-r--r--	WfProofs.v	8521	log plain
-rw-r--r--	WfReflective.v	13719	log plain
-rw-r--r--	WfReflectiveGen.v	17244	log plain
d---------	Z	377	log plain