fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Interpret syntax with Let_In	Jason Gross	2016-10-31
\|
*	Add interp_type_gen_rel_pointwise2, _gen =>	Jason Gross	2016-10-28
\|
*	Add arguments to mapf_interp_flat_type_gen	Jason Gross	2016-10-27
\|
*	Small example of bounds-calculation with dependent types (#61)	Jason Gross	2016-09-29
	This might properly belong in Experiments rather than TestCase. It demos the ability to transform from one kind of constants to another kind, and to plug bounds calculation functions into [var] to get bounds. There's not currently any sort of correctness theorem, and I'm not entirely sure what one would look like. Probably something that says that if you map a function over the syntax tree and then interpret, you could instead have first interpreted and then applied the function. I'm hopeful that this will provide a template for integrating this version of the syntax with rsloan-phoas.