fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Reorder arguments to Wf_MapCast for eauto	Jason Gross	2017-03-30
\| \| \| \|	This way we pick up the equality hypothesis first.
*	Don't linearize and eta in MapCastByDeBruijn	Jason Gross	2017-03-30
\|
*	Add Wf_MapCast_arrow	Jason Gross	2017-03-28
\|
*	Add Wf_MapCast to wf database	Jason Gross	2017-03-28
\|
*	Break up MapCast into separate pieces for easier debugging	Jason Gross	2017-03-28
\|
*	Finish proof of wf_map_cast	Jason Gross	2017-03-28
\| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change --------------------------------------------------------------------- 0m20.75s \| Total \| 0m15.19s \|\| +0m05.56s --------------------------------------------------------------------- 0m19.33s \| Reflection/Named/MapCastWf \| 0m13.82s \|\| +0m05.50s 0m00.79s \| Reflection/MapCastByDeBruijnInterp \| 0m00.75s \|\| +0m00.04s 0m00.64s \| Reflection/MapCastByDeBruijnWf \| 0m00.62s \|\| +0m00.02s
*	Add aborted MapCastByDeBruijnWf	Jason Gross	2017-03-19
	I'm not sure exactly why the wf proof requires cast_backb in map_cast; it seems to be used as a dumb way of instantiating the context-extension on the input expression tree (since we're only given the context-extension values on the output expression, which has a different type).